diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -21,7 +21,10 @@
   val from_polyml: PolyML_Pretty.pretty -> pretty
   val format_polyml: int -> PolyML_Pretty.pretty -> string
   val format: int -> pretty -> string
-  val make_string_fn: string -> string
+  val default_margin: int
+  val string_of_polyml: PolyML_Pretty.pretty -> string
+  val make_string_global: string
+  val make_string_local: string -> string
 end;
 
 structure ML_Pretty: ML_PRETTY =
@@ -99,21 +102,17 @@
 
 fun format margin = format_polyml margin o to_polyml;
 
+val default_margin = 76;
+
 
 (* make string *)
 
-local
-  fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
-  fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
-in
+val string_of_polyml = format_polyml default_margin;
 
-fun make_string_fn local_env =
-  if local_env <> "" then
-    pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
-  else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
-    pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()")
-  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
+fun make_string depth =
+  "(fn x => ML_Pretty.string_of_polyml (ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))))";
+
+val make_string_global = make_string "ML_Print_Depth.get_print_depth ()";
+fun make_string_local local_env = make_string (local_env ^ ".ML_print_depth ()");
 
 end;
-
-end;