# HG changeset patch
# User wenzelm
# Date 1192205352 -7200
# Node ID 61946780de00fae6af31794386d29da68061edc7
# Parent  38f4ecb71e8c1e358badba778fa4e5a102d7f8a7
eval_term: moved actual evaluation out of CRITICAL section;

diff -r 38f4ecb71e8c -r 61946780de00 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Oct 12 15:46:29 2007 +0200
+++ b/src/Pure/codegen.ML	Fri Oct 12 18:09:12 2007 +0200
@@ -1013,26 +1013,28 @@
 
 val eval_result = ref (fn () => Bound 0);
 
-fun eval_term thy = PrintMode.setmp [] (fn t =>
-  let
-    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
-      error "Term to be evaluated contains type variables";
-    val _ = (null (term_vars t) andalso null (term_frees t)) orelse
-      error "Term to be evaluated contains variables";
-    val (code, gr) = setmp mode ["term_of"]
-      (generate_code_i thy [] "Generated")
-      [("result", Abs ("x", TFree ("'a", []), t))];
-    val s = "structure EvalTerm =\nstruct\n\n" ^
-      space_implode "\n" (map snd code) ^
-      "\nopen Generated;\n\n" ^ Pretty.string_of
-        (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
-          Pretty.brk 1,
-          mk_app false (mk_term_of gr "Generated" false (fastype_of t))
-            [Pretty.str "(result ())"],
-          Pretty.str ");"]) ^
-      "\n\nend;\n";
-    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
-  in !eval_result () end);
+fun eval_term thy t =
+  let val e = PrintMode.setmp [] (fn () =>
+    let
+      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+        error "Term to be evaluated contains type variables";
+      val _ = (null (term_vars t) andalso null (term_frees t)) orelse
+        error "Term to be evaluated contains variables";
+      val (code, gr) = setmp mode ["term_of"]
+        (generate_code_i thy [] "Generated")
+        [("result", Abs ("x", TFree ("'a", []), t))];
+      val s = "structure EvalTerm =\nstruct\n\n" ^
+        space_implode "\n" (map snd code) ^
+        "\nopen Generated;\n\n" ^ Pretty.string_of
+          (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
+            Pretty.brk 1,
+            mk_app false (mk_term_of gr "Generated" false (fastype_of t))
+              [Pretty.str "(result ())"],
+            Pretty.str ");"]) ^
+        "\n\nend;\n";
+      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
+    in !eval_result end) ();
+  in e () end;
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
   let