src/Tools/Code/code_runtime.ML
changeset 69623 ef02c5e051e5
parent 69597 ff784d5a5bfb
child 69742 170daa8170be
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Jan 07 18:50:41 2019 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 10 12:07:05 2019 +0000
     1.3 @@ -437,7 +437,7 @@
     1.4      val thy = Proof_Context.theory_of ctxt;
     1.5      val (ml_modules, target_names) =
     1.6        Code_Target.produce_code_for ctxt
     1.7 -        target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
     1.8 +        target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
     1.9      val ml_code = space_implode "\n\n" (map snd ml_modules);
    1.10      val (consts', tycos') = chop (length consts) target_names;
    1.11      val consts_map = map2 (fn const =>
    1.12 @@ -856,7 +856,7 @@
    1.13    |-> (fn ([Const (const, _)], _) =>
    1.14      Code_Target.set_printings (Constant (const,
    1.15        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
    1.16 -  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN []));
    1.17 +  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
    1.18  
    1.19  fun process_file filepath (definienda, thy) =
    1.20    let