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