--- 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;