src/Pure/ROOT.ML
changeset 21941 62dd79056d70
parent 21930 918fb0fb5c72
child 22108 d76ea9928959
--- 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;