--- a/src/Tools/Code/code_printer.ML Sat May 08 16:53:53 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Sat May 08 19:14:13 2010 +0200
@@ -116,8 +116,8 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = PrintMode.setmp [] (Pretty.indent i);
-fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n";
-fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p;
+fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
(** names and variable name contexts **)