# HG changeset patch
# User haftmann
# Date 1193313125 -7200
# Node ID e1146aa1e3e3fdf05d3f9ef76c6aad106581534c
# Parent  5cd8486c5a4f93c440187c33685905267623338c
tuned

diff -r 5cd8486c5a4f -r e1146aa1e3e3 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Thu Oct 25 13:52:04 2007 +0200
+++ b/src/Tools/code/code_target.ML	Thu Oct 25 13:52:05 2007 +0200
@@ -1707,17 +1707,10 @@
       (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
     val code' = CodeThingol.add_value_stmt (t, ty) code;
-    fun eval () = (
-      reff := NONE;
-      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
-      );
-  in CRITICAL eval () end;
+    val label = "evaluation in SML";
+    fun eval () = (seri (SOME [CodeName.value_name]) code';
+      evaluate (ref_name, reff) label Output.ml_output (!eval_verbose) val_args);
+  in NAMED_CRITICAL label eval end;