src/Pure/ROOT.ML
changeset 21930 918fb0fb5c72
parent 21890 3fb9762ba701
child 21941 62dd79056d70
     1.1 --- a/src/Pure/ROOT.ML	Fri Dec 29 16:46:39 2006 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Dec 29 16:47:49 2006 +0100
     1.3 @@ -86,9 +86,9 @@
     1.4  (* Next line is OLD CODE: in case you have problems, uncomment next line and 
     1.5     comment out line after. Please report any problems to da@inf.ed.ac.uk.
     1.6     Plan is to remove old code very soon. *)
     1.7 -(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; 
     1.8 -(* Next line is NEW CODE.  Currently broken on SMLNJ. *)
     1.9 -(* cd "ProofGeneral"; use "ROOT.ML"; cd "..";  new code *)
    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  
    1.14  use_thy "Pure";
    1.15  structure Pure = struct val thy = theory "Pure" end;