--- a/src/HOL/Main.thy Mon Oct 29 10:37:09 2007 +0100
+++ b/src/HOL/Main.thy Mon Oct 29 16:13:41 2007 +0100
@@ -13,6 +13,6 @@
PreList} already includes most HOL theories.
*}
-ML {* val HOL_proofs = !proofs *}
+ML {* val HOL_proofs = ! Proofterm.proofs *}
end