src/Pure/ROOT.ML
changeset 21941 62dd79056d70
parent 21930 918fb0fb5c72
child 22108 d76ea9928959
     1.1 --- a/src/Pure/ROOT.ML	Fri Dec 29 18:25:46 2006 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Dec 29 18:46:01 2006 +0100
     1.3 @@ -83,12 +83,7 @@
     1.4  cd "Tools"; use "ROOT.ML"; cd "..";
     1.5  
     1.6  (*configuration for Proof General*)
     1.7 -(* Next line is OLD CODE: in case you have problems, uncomment next line and 
     1.8 -   comment out line after. Please report any problems to da@inf.ed.ac.uk.
     1.9 -   Plan is to remove old code very soon. *)
    1.10 -(*(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; *)
    1.11 -(* Next line is NEW CODE.  Hopefully now working on SMLNJ and Poly/ML. *)
    1.12 -cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
    1.13 +cd "ProofGeneral"; use "ROOT.ML"; cd "..";
    1.14  
    1.15  use_thy "Pure";
    1.16  structure Pure = struct val thy = theory "Pure" end;