src/Tools/Code/code_scala.ML
changeset 38916 c0b857a04758
parent 38915 026526cba0e6
child 38922 ec2a8efd8990
--- a/src/Tools/Code/code_scala.ML	Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 16:33:06 2010 +0200
@@ -483,7 +483,7 @@
     fun write width NONE = writeln_pretty width
       | write width (SOME p) = File.write p o string_of_pretty width;
   in
-    Code_Target.mk_serialization write (rpair [] oo string_of_pretty) p
+    Code_Target.serialization write (rpair [] oo string_of_pretty) p
   end;
 
 end; (*local*)