changeset 39102 | 4ae1d212100f |
parent 39059 | 3a11a667af75 |
child 39142 | f63715f00fdd |
child 39147 | 3c284a152bd6 |
--- a/src/Tools/Code/code_scala.ML Thu Sep 02 17:02:00 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Sep 02 19:08:48 2010 +0200 @@ -389,7 +389,7 @@ fun write width NONE = writeln o format [] width | write width (SOME p) = File.write p o format [] width; in - Code_Target.serialization write (rpair [] ooo format) p + Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p end; val serializer : Code_Target.serializer =