--- a/src/HOL/Import/ROOT.ML Sat Nov 10 14:31:23 2007 +0100
+++ b/src/HOL/Import/ROOT.ML Sat Nov 10 14:36:33 2007 +0100
@@ -3,6 +3,6 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-proofs := 0;
+Proofterm.proofs := 0;
use_thy "HOL4Compat";
use_thy "HOL4Syntax";