# HG changeset patch
# User aspinall
# Date 1166636307 -3600
# Node ID 682dbe9478623bd81f14212866f46f5f7d9c1b01
# Parent  c75a44597fb76158b46cfffd69a07d3f4bb7085c
Use new Proof General code by default [see comment for reverting]

diff -r c75a44597fb7 -r 682dbe947862 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 20 17:03:46 2006 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 20 18:38:27 2006 +0100
@@ -83,9 +83,11 @@
 cd "Tools"; use "ROOT.ML"; cd "..";
 
 (*configuration for Proof General*)
-(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML";
-(* NEW PG code: [ in testing ]
-cd "ProofGeneral"; use "ROOT.ML"; cd ".."; *)
+(* 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_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;