--- a/src/Tools/Code/code_eval.ML Tue Aug 31 16:07:30 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Tue Aug 31 16:23:58 2010 +0200
@@ -51,11 +51,11 @@
|> Graph.new_node (value_name,
Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
|> 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 " ^ Long_Name.base_name value_name'
- ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
- in ML_Context.evaluate ctxt false reff sml_code end;
+ val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
+ (the_default target some_target) NONE (SOME "Code") [] naming program' [value_name];
+ val value_code = space_implode " "
+ (value_name' :: map (enclose "(" ")") args);
+ in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;