diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -62,7 +62,7 @@
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
-  in Code_Thingol.eval thy postproc evaluator t end;
+  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
 
 
 (** instrumentalization by antiquotation **)