X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8aa9e828875c13a969005edbdcc30ab4976b704d;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=4a2fdc561428f8924689839f0128e859f5d556cf;hpb=0c62b48dd8d961279e780f6fbc2a915d18b77b92;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4a2fdc561..8aa9e8288 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2016,8 +2016,8 @@ let searchPattern () =
           let html =
            " <h1>Backward Query: </h1>" ^
            " <h2>Levels: </h2> " ^
-           MQueryGenerator.string_of_levels
-            (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+           MQueryLevels.string_of_levels
+            (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
 	   " <pre>" ^ get_last_query result ^ "</pre>"
           in
            output_html outputhtml html ;