removed obsolete install_pp.ML (cf. pure_setup.ML);
--- a/src/Pure/IsaMakefile Sun Jul 29 14:30:07 2007 +0200
+++ b/src/Pure/IsaMakefile Sun Jul 29 16:00:00 2007 +0200
@@ -65,7 +65,7 @@
Tools/nbe_eval.ML Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML \
codegen.ML compress.ML config_option.ML conjunction.ML consts.ML context.ML \
context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \
- fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML \
+ fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML \
more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \
pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
--- a/src/Pure/install_pp.ML Sun Jul 29 14:30:07 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/install_pp.ML
- ID: $Id$
-
-ML toplevel pretty printing.
-*)
-
-install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
-install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));