src/Pure/install_pp.ML
changeset 3509 db03a42120bf
parent 1528 608dd813b437
child 11885 427d80b807c7
     1.1 --- a/src/Pure/install_pp.ML	Wed Jul 09 16:52:51 1997 +0200
     1.2 +++ b/src/Pure/install_pp.ML	Wed Jul 09 16:53:53 1997 +0200
     1.3 @@ -4,15 +4,10 @@
     1.4  Set up automatic toplevel pretty printing.
     1.5  *)
     1.6  
     1.7 -fun init_pps () =
     1.8 -  use_string
     1.9 -   ["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);",
    1.10 -    "install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
    1.11 -    "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
    1.12 -    "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
    1.13 -    "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",
    1.14 -    "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);",
    1.15 -    "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"];
    1.16 -
    1.17 -init_pps ();
    1.18 -
    1.19 +install_pp (make_pp ["Theory", "theory"] pprint_theory);
    1.20 +install_pp (make_pp ["Thm", "thm"] pprint_thm);
    1.21 +install_pp (make_pp ["Thm", "cterm"] pprint_cterm);
    1.22 +install_pp (make_pp ["Thm", "ctyp"] pprint_ctyp);
    1.23 +install_pp (make_pp ["Sign", "sg"] Sign.pprint_sg);
    1.24 +install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    1.25 +install_pp (make_pp ["typ"] Syntax.simple_pprint_typ);