X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=e06950508c72ec5570e6667b33fb1fe9def8df97;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=b5dea98164bb026c584c2979defa58fb9d46cf9f;hpb=ebc346f535472bc0f5075dac48040ea5ecc40232;p=helm.git

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index b5dea9816..e06950508 100644
--- 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