--- 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;