src/Tools/code/code_ml.ML
changeset 30672 beaadd5af500
parent 30648 17365ef082f3
child 30675 2e796219f441
--- a/src/Tools/code/code_ml.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Tools/code/code_ml.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -969,7 +969,7 @@
         val (value_code, [SOME value_name']) = ml_code_of thy 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 Output.ml_output false reff sml_code end;
+      in ML_Context.evaluate ctxt false reff sml_code end;
   in eval'' thy (rpair eval') ct end;
 
 fun eval_term reff = eval Code_Thingol.eval_term I reff;