1.1 --- a/src/Tools/Code/code_ml.ML	Thu Jul 08 16:28:18 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 08 16:41:57 2010 +0200
     1.3 @@ -907,7 +907,7 @@
     1.4          error ("Unknown statement name: " ^ labelled_name name);
     1.5    in (deresolver, nodes) end;
     1.6  
     1.7 -fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
     1.8 +fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
     1.9    reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    1.10    let
    1.11      val is_cons = Code_Thingol.is_cons program;
    1.12 @@ -938,7 +938,6 @@
    1.13      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
    1.14    in
    1.15      Code_Target.mk_serialization target
    1.16 -      (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE)
    1.17        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
    1.18        (rpair stmt_names' o code_of_pretty) p destination
    1.19    end;
    1.20 @@ -950,7 +949,7 @@
    1.21  
    1.22  fun evaluation_code_of thy target struct_name =
    1.23    Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
    1.24 -    serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
    1.25 +    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
    1.26  
    1.27  
    1.28  (** formal checking of compiled code **)
    1.29 @@ -969,12 +968,11 @@
    1.30  fun isar_seri_sml module_name =
    1.31    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.32    >> (fn with_signatures => serialize_ml target_SML
    1.33 -      (SOME (use_text ML_Env.local_context (1, "generated code") false))
    1.34        print_sml_module print_sml_stmt module_name with_signatures));
    1.35  
    1.36  fun isar_seri_ocaml module_name =
    1.37    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.38 -  >> (fn with_signatures => serialize_ml target_OCaml NONE
    1.39 +  >> (fn with_signatures => serialize_ml target_OCaml
    1.40        print_ocaml_module print_ocaml_stmt module_name with_signatures));
    1.41  
    1.42  val setup =