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

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

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

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

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

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