removed obsolete install_pp.ML (cf. pure_setup.ML);
authorwenzelm
Sun, 29 Jul 2007 16:00:00 +0200
changeset 24052 90dd4df2c7c3
parent 24051 896fb015079c
child 24053 af1dd276fae0
removed obsolete install_pp.ML (cf. pure_setup.ML);
src/Pure/IsaMakefile
src/Pure/install_pp.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));