src/Pure/ROOT.ML
changeset 21890 3fb9762ba701
parent 21889 682dbe947862
child 21930 918fb0fb5c72
     1.1 --- a/src/Pure/ROOT.ML	Wed Dec 20 18:38:27 2006 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Dec 21 08:42:53 2006 +0100
     1.3 @@ -86,8 +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 -cd "ProofGeneral"; use "ROOT.ML"; cd "..";  (* new code *)
     1.9 +(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; 
    1.10 +(* Next line is NEW CODE.  Currently broken on SMLNJ. *)
    1.11 +(* cd "ProofGeneral"; use "ROOT.ML"; cd "..";  new code *)
    1.12  
    1.13  use_thy "Pure";
    1.14  structure Pure = struct val thy = theory "Pure" end;