qualified Proofterm.proofs;

--- 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

--- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -217,7 +217,7 @@
   end;
 
 fun add_dt_realizers names thy =
-  if !proofs < 2 then thy
+  if ! Proofterm.proofs < 2 then thy
   else let
     val _ = message "Adding realizers for induction and case analysis ..."
     val infos = map (DatatypePackage.the_datatype thy) names;

--- a/src/Pure/ProofGeneral/ROOT.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/Pure/ProofGeneral/ROOT.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -15,7 +15,7 @@
 
 use "pgip_isabelle.ML";
 use "pgml_isabelle.ML";
-(use |> setmp proofs 1 |> setmp quick_and_dirty true) "preferences.ML";
+(use |> setmp Proofterm.proofs 1 |> setmp quick_and_dirty true) "preferences.ML";
 use "pgip_parser.ML";
 
 use "parsing.ML";   (* old version *)

--- a/src/Pure/ProofGeneral/preferences.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -57,8 +57,8 @@
 
 val proof_pref =
     let
-        fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
-        fun set s = proofs := (if PgipTypes.read_pgipbool s then 2 else 1)
+        fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2)
+        fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1)
     in
         mkpref get set PgipTypes.Pgipbool "full-proofs"
                "Record full proof objects internally"

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -579,7 +579,7 @@
 
 fun set_proverflag_thmdeps b =
     (show_theorem_dependencies := b;
-     proofs := (if b then 1 else 2))
+     Proofterm.proofs := (if b then 1 else 2))
 
 fun setproverflag (Setproverflag vs) =
     let 

--- a/src/Pure/pure_setup.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/Pure/pure_setup.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -44,4 +44,4 @@
 val cd = File.cd o Path.explode;
 ml_prompts "ML> " "ML# ";
 
-proofs := 0;
+Proofterm.proofs := 0;