diff -r d53d1a16d5ee -r 248de8dd839e src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -12,19 +12,6 @@
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 
-(* toplevel pretty printers *)
-
-structure ML_Pretty =
-struct
-  datatype context = datatype PolyML.context;
-  datatype pretty = datatype PolyML.pretty;
-end;
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
 (* runtime compilation *)
 
 structure ML_NameSpace =
@@ -81,3 +68,16 @@
   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 end;
+
+
+(* toplevel pretty printing *)
+
+fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
+  | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+  | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
+  | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+    ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+