first moogle template checkin

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

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index b5dea98164bb026c584c2979defa58fb9d46cf9f..e06950508c72ec5570e6667b33fb1fe9def8df97 100644 (file)
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -211,8 +211,12 @@ module Make(C:DisambiguateTypes.Callbacks) =
        in
         debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
         let environment',metasenv,expr =
-         Disambiguate'.disambiguate_term mqi_handle 
-          context metasenv (Mathml_editor.get_tex tex_editor) !environment
+         match
+          Disambiguate'.disambiguate_term mqi_handle 
+           context metasenv (Mathml_editor.get_tex tex_editor) !environment
+         with
+            [environment',metasenv,expr] -> environment',metasenv,expr
+          | _ -> assert false
         in
          environment := environment' ;
          metasenv,expr