src/Tools/Code/code_eval.ML

         val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
           (the_default target some_target) "" naming program' [value_name];
         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 **)
 
 local