src/Tools/Code/code_ml.ML
changeset 38915 026526cba0e6
parent 38913 d1d4d808be26
child 38916 c0b857a04758
     1.1 --- a/src/Tools/Code/code_ml.ML	Mon Aug 30 16:25:04 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 16:31:38 2010 +0200
     1.3 @@ -934,10 +934,10 @@
     1.4      val stmt_names' = (map o try)
     1.5        (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
     1.6      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
     1.7 +    fun write width NONE = writeln_pretty width
     1.8 +      | write width (SOME p) = File.write p o string_of_pretty width;
     1.9    in
    1.10 -    Code_Target.mk_serialization
    1.11 -      (fn width => (fn NONE => writeln_pretty width | SOME file => File.write file o string_of_pretty width))
    1.12 -      (fn width => (rpair stmt_names' o string_of_pretty width)) p
    1.13 +    Code_Target.mk_serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
    1.14    end;
    1.15  
    1.16  end; (*local*)