--- a/src/HOL/ROOT.ML Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/ROOT.ML Sun Dec 14 18:45:51 2008 +0100
@@ -3,6 +3,7 @@
Classical Higher-order Logic -- batteries included.
*)
+set new_locales;
use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;