diff -r 97b715e65f70 -r a0342b27b38e src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Mon Sep 26 17:35:45 1994 +0100
+++ b/src/Pure/install_pp.ML	Mon Sep 26 17:36:10 1994 +0100
@@ -1,19 +1,18 @@
 (*  Title:      Pure/install_pp.ML
     ID:         $Id$
 
-Set up automatic toplevel printing.
+Set up automatic toplevel pretty printing.
 *)
 
-install_pp (make_pp ["Thm", "thm"] pprint_thm);
-install_pp (make_pp ["Thm", "theory"] pprint_theory);
-install_pp (make_pp ["Thm", "cterm"] pprint_cterm);
-install_pp (make_pp ["Thm", "ctyp"] pprint_ctyp);
-install_pp (make_pp ["Sign", "sg"] Sign.pprint_sg);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] Syntax.simple_pprint_typ);
+fun init_pps () =
+  use_string
+   ["install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
+    "install_pp (make_pp [\"Thm\", \"theory\"] pprint_theory);",
+    "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
+    "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
+    "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",
+    "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);",
+    "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"];
 
-(*
-install_pp (make_pp ["term"] pprint_term);
-install_pp (make_pp ["typ"] pprint_typ);
-*)
+init_pps ();