--- a/src/Pure/General/pretty.ML Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/General/pretty.ML Thu Apr 07 13:35:08 2016 +0200
@@ -334,7 +334,7 @@
(* output interfaces *)
-val margin_default = Unsynchronized.ref 76; (*right margin, or page width*)
+val margin_default = Unsynchronized.ref ML_Pretty.default_margin; (*right margin, or page width*)
val symbolicN = "pretty_symbolic";
@@ -406,3 +406,9 @@
val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
end;
+
+structure ML_Pretty =
+struct
+ open ML_Pretty;
+ val string_of_polyml = Pretty.string_of o Pretty.from_polyml;
+end;