src/Tools/Code/code_ml.ML
changeset 39102 4ae1d212100f
parent 39061 9b1fd2df743c
child 39142 f63715f00fdd
child 39147 3c284a152bd6
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 17:02:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 19:08:48 2010 +0200
     1.3 @@ -809,12 +809,11 @@
     1.4          o rev o flat o Graph.strong_conn) nodes
     1.5        |> split_list
     1.6        |> (fn (decls, body) => (flat decls, body))
     1.7 -    val names' = map (try (deresolver [])) names;
     1.8      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     1.9      fun write width NONE = writeln o format [] width
    1.10        | write width (SOME p) = File.write p o format [] width;
    1.11    in
    1.12 -    Code_Target.serialization write (rpair names' ooo format) p
    1.13 +    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
    1.14    end;
    1.15  
    1.16  val serializer_sml : Code_Target.serializer =