src/Tools/Code/code_runtime.ML
changeset 55683 5732a55b9232
parent 55304 55ac31bc08a4
child 55684 ee49b4f7edc8
--- a/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
@@ -199,7 +199,7 @@
     val program = Code_Thingol.consts_program thy consts;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for thy
-        target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
+        target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
     val ml_code = space_implode "\n\n" (map snd ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
@@ -440,7 +440,7 @@
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
-  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
+  #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
 
 fun process_file filepath (definienda, thy) =
   let