# HG changeset patch
# User wenzelm
# Date 868460033 -7200
# Node ID db03a42120bfd3f2af8d8e4ef4f2c1888be91723
# Parent  089806e6133b6f89f69d37b68a937e582f1fbad9
removed init_pps;

diff -r 089806e6133b -r db03a42120bf src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Wed Jul 09 16:52:51 1997 +0200
+++ b/src/Pure/install_pp.ML	Wed Jul 09 16:53:53 1997 +0200
@@ -4,15 +4,10 @@
 Set up automatic toplevel pretty printing.
 *)
 
-fun init_pps () =
-  use_string
-   ["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);",
-    "install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
-    "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);"];
-
-init_pps ();
-
+install_pp (make_pp ["Theory", "theory"] pprint_theory);
+install_pp (make_pp ["Thm", "thm"] pprint_thm);
+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);