Disable new Proof General code until SML/NJ compile fixed.
authoraspinall
Thu, 21 Dec 2006 08:42:53 +0100
changeset 21890 3fb9762ba701
parent 21889 682dbe947862
child 21891 b4e4ea3db161
Disable new Proof General code until SML/NJ compile fixed.
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 20 18:38:27 2006 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 21 08:42:53 2006 +0100
@@ -86,8 +86,9 @@
 (* 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";  *)
-cd "ProofGeneral"; use "ROOT.ML"; cd "..";  (* new code *)
+(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; 
+(* Next line is NEW CODE.  Currently broken on SMLNJ. *)
+(* cd "ProofGeneral"; use "ROOT.ML"; cd "..";  new code *)
 
 use_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;