diff -r 765528b4b419 -r 30ce1e078b72 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Thu Oct 18 16:09:38 2007 +0200
+++ b/src/Tools/code/code_target.ML	Thu Oct 18 16:09:39 2007 +0200
@@ -1694,8 +1694,8 @@
   in
     project
     #> check_empty_funs
-    #> seri module file args (CodeName.labelled_name thy) reserved includes (Symtab.lookup alias)
-        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
+    #> seri module file args (CodeName.labelled_name thy) reserved includes
+        (Symtab.lookup alias) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   end;
 
 fun eval_invoke thy (ref_name, reff) code (t, ty) args =
@@ -1705,21 +1705,18 @@
     val val_args = space_implode " "
       (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
-    fun eval code = (
+    val code' = CodeThingol.add_value_stmt (t, ty) code;
+    fun eval () = (
       reff := NONE;
-      seri (SOME [CodeName.value_name]) code;
+      seri (SOME [CodeName.value_name]) code';
       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
         ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
       case !reff
        of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
             ^ " (reference probably has been shadowed)")
-        | SOME f => f ()
+        | SOME f => f
       );
-  in
-    code
-    |> CodeThingol.add_value_stmt (t, ty)
-    |> eval
-  end;
+  in CRITICAL eval () end;