X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=cbaa08721cca870b1643e5005cbf7a62ae4a6825;hb=59945285cda6b39178eeffedb32a37d3141fe844;hp=0234c4824673837682dae785401920ab7abcd0ad;hpb=eb9ca860db8cb06083765f7698179f16dee5303e;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 0234c4824..cbaa08721 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -118,19 +118,7 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let b = 
-        try
-          GrafiteSync.push ();
-          LexiconSync.push ();
-          let rc = MatitacLib.Make.make root [tgt] in 
-          LexiconSync.pop ();
-          GrafiteSync.pop ();
-          rc
-        with 
-        | exn ->
-            HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
-            assert false
-      in
+      let b = MatitacLib.Make.make root [tgt] in
       if b then 
         try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
          raise