--- a/src/HOL/ROOT.ML Fri Dec 19 15:05:37 2008 +0100
+++ b/src/HOL/ROOT.ML Fri Dec 19 16:39:23 2008 +0100
@@ -3,7 +3,6 @@
Classical Higher-order Logic -- batteries included.
*)
-set new_locales;
use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;