src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Mon Dec 28 23:34:36 2009 +0100
+++ b/src/HOL/ROOT.ML	Tue Dec 29 16:20:39 2009 +0100
@@ -1,5 +1,3 @@
 (* Classical Higher-order Logic -- batteries included *)
 
 use_thys ["Complex_Main"];
-
-val HOL_proofs = ! Proofterm.proofs;