# HG changeset patch
# User wenzelm
# Date 1167414361 -3600
# Node ID 62dd79056d706ea9fd9dc115d0dfeb8ca6f776d4
# Parent  fbd068dd4d29618221cbdf87a01c9633d8062228
removed obsolete proof_general.ML;

diff -r fbd068dd4d29 -r 62dd79056d70 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Dec 29 18:25:46 2006 +0100
+++ b/src/Pure/IsaMakefile	Fri Dec 29 18:46:01 2006 +0100
@@ -67,9 +67,9 @@
   conjunction.ML consts.ML context.ML defs.ML display.ML drule.ML		\
   envir.ML fact_index.ML goal.ML install_pp.ML library.ML logic.ML		\
   meta_simplifier.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML		\
-  proof_general.ML proofterm.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 type_infer.ML unify.ML variable.ML
+  proofterm.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		\
+  type_infer.ML unify.ML variable.ML
 	@./mk
 
 
diff -r fbd068dd4d29 -r 62dd79056d70 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Dec 29 18:25:46 2006 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 29 18:46:01 2006 +0100
@@ -83,12 +83,7 @@
 cd "Tools"; use "ROOT.ML"; cd "..";
 
 (*configuration for Proof General*)
-(* Next line is OLD CODE: in case you have problems, uncomment next line and 
-   comment out line after. Please report any problems to da@inf.ed.ac.uk.
-   Plan is to remove old code very soon. *)
-(*(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; *)
-(* Next line is NEW CODE.  Hopefully now working on SMLNJ and Poly/ML. *)
-cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
+cd "ProofGeneral"; use "ROOT.ML"; cd "..";
 
 use_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;