--- 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
--- 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;