# HG changeset patch
# User wenzelm
# Date 1185717600 -7200
# Node ID 90dd4df2c7c39b81ab081e0ca06db1dee55f1637
# Parent  896fb015079cfc6e4153649356cccea5933dcce8
removed obsolete install_pp.ML (cf. pure_setup.ML);

diff -r 896fb015079c -r 90dd4df2c7c3 src/Pure/IsaMakefile
--- 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		\
diff -r 896fb015079c -r 90dd4df2c7c3 src/Pure/install_pp.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));