Generator updated for new MathQL.ml

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4a2fdc561428f8924689839f0128e859f5d556cf..8aa9e828875c13a969005edbdcc30ab4976b704d 100644 (file)
--- 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 ;