changeset 38916 | c0b857a04758 |
parent 38915 | 026526cba0e6 |
child 38921 | 15f8cffdbf5d |
--- a/src/Tools/Code/code_ml.ML Mon Aug 30 16:31:38 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Mon Aug 30 16:33:06 2010 +0200 @@ -937,7 +937,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 (fn width => (rpair stmt_names' o string_of_pretty width)) p + Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p end; end; (*local*)