diff -r 6e1f3d609a68 -r 403585a89772 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat May 08 16:53:53 2010 +0200
+++ b/src/Pure/codegen.ML	Sat May 08 19:14:13 2010 +0200
@@ -109,9 +109,7 @@
 
 val margin = Unsynchronized.ref 80;
 
-fun string_of p = (Pretty.string_of |>
-  PrintMode.setmp [] |>
-  Pretty.setmp_margin_CRITICAL (!margin)) p;
+fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
 
 val str = PrintMode.setmp [] Pretty.str;