diff -r 928c5a5bdc93 -r 4ae1d212100f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 19:08:48 2010 +0200
@@ -809,12 +809,11 @@
         o rev o flat o Graph.strong_conn) nodes
       |> split_list
       |> (fn (decls, body) => (flat decls, body))
-    val names' = map (try (deresolver [])) names;
     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
   in
-    Code_Target.serialization write (rpair names' ooo format) p
+    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   end;
 
 val serializer_sml : Code_Target.serializer =