tuned;

--- a/src/Pure/General/secure.ML	Wed Feb 17 23:15:47 2016 +0100
+++ b/src/Pure/General/secure.ML	Wed Feb 17 23:28:58 2016 +0100
@@ -13,7 +13,6 @@
   val use_text: use_context ->
     {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
   val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
-  val toplevel_pp: string list -> string -> unit
 end;
 
 structure Secure: SECURE =
@@ -36,11 +35,8 @@
 
 val raw_use_text = use_text;
 val raw_use_file = use_file;
-val raw_toplevel_pp = toplevel_pp;
 
 fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
 fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
 
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
 end;

--- a/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 23:15:47 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 23:28:58 2016 +0100
@@ -1,9 +1,63 @@
 (*  Title:      Pure/ML/install_pp_polyml.ML
     Author:     Makarius
 
-Extra toplevel pretty-printing for Poly/ML.
+ML toplevel pretty-printing for Poly/ML.
 *)
 
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
+  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
+  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
+  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
+  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
+  ml_pretty (Pretty.to_ML (Pretty.position pos)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
+  ml_pretty (Pretty.to_ML (Binding.pp binding)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
+  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
+  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
+  ml_pretty (Pretty.to_ML (Path.pretty path)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
+  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
+  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
+  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
+  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
 
@@ -107,4 +161,3 @@
 end;
 
 end;
-

--- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:15:47 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:28:58 2016 +0100
@@ -189,10 +189,6 @@
 if ML_System.name = "polyml-5.6"
 then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
 
-fun toplevel_pp context (_: string list) pp =
-  use_text context {line = 1, file = "pp", verbose = false, debug = false}
-    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
-
 fun ml_make_string struct_name =
   "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
     struct_name ^ ".ML_print_depth ())))))";

--- a/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
+++ b/src/Pure/ROOT.ML	Wed Feb 17 23:28:58 2016 +0100
@@ -47,8 +47,6 @@
       Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
         handle ERROR msg => (writeln msg; error "ML error")) ();
 
-val toplevel_pp = Secure.toplevel_pp;
-
 
 
 (** bootstrap phase 1: towards ML within Isar context *)
@@ -333,27 +331,6 @@
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
 
-(* ML toplevel pretty printing *)
-
-toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
-toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
-toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
-toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
-toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Binding.pp";
-toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
-toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
-toplevel_pp ["Context", "theory"] "Context.pretty_thy";
-toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
-toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Path.pretty";
-toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
-toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
-toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
-
 use "ML/install_pp_polyml.ML";