# HG changeset patch
# User aspinall
# Date 1166686973 -3600
# Node ID 3fb9762ba7017bd53e63258d57bca847a93af24d
# Parent  682dbe9478623bd81f14212866f46f5f7d9c1b01
Disable new Proof General code until SML/NJ compile fixed.

diff -r 682dbe947862 -r 3fb9762ba701 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;