src/Tools/Code/code_eval.ML
changeset 38928 0e6f54c9d201
parent 38923 79d7f2b4cf71
child 38929 d9ac9dee764d
--- a/src/Tools/Code/code_eval.ML	Tue Aug 31 14:43:27 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 15:08:04 2010 +0200
@@ -59,7 +59,7 @@
           |> fold (curry Graph.add_edge value_name) deps;
         val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy
           (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []);
-        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
+        val sml_code = "let\n" ^ value_code ^ "\nin " ^ Long_Name.base_name value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
   in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;