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*)