diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Mon Jan 07 18:50:41 2019 +0100 +++ b/src/Tools/Code/code_runtime.ML Thu Jan 10 12:07:05 2019 +0000 @@ -437,7 +437,7 @@ val thy = Proof_Context.theory_of ctxt; val (ml_modules, target_names) = Code_Target.produce_code_for ctxt - target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos); + target module_name NONE [] 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 => @@ -856,7 +856,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 (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN [])); + #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE [])); fun process_file filepath (definienda, thy) = let