# HG changeset patch
# User aspinall
# Date 1167407269 -3600
# Node ID 918fb0fb5c72959c1012ac1c350a75ec6162e974
# Parent  fb0cd849bc607ff95d580c754e0bbee39d7ad80f
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.

diff -r fb0cd849bc60 -r 918fb0fb5c72 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Dec 29 16:46:39 2006 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 29 16:47:49 2006 +0100
@@ -86,9 +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"; 
-(* Next line is NEW CODE.  Currently broken on SMLNJ. *)
-(* 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.  Hopefully now working on SMLNJ and Poly/ML. *)
+cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
 
 use_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;