# HG changeset patch # User wenzelm # Date 1193670821 -3600 # Node ID 7463251e72736cddcf11f703544826c714893e9e # Parent 78943ac46f6d37a27103a35b931c9353c240ac14 qualified Proofterm.proofs; diff -r 78943ac46f6d -r 7463251e7273 src/HOL/Main.thy --- 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 diff -r 78943ac46f6d -r 7463251e7273 src/HOL/Tools/datatype_realizer.ML --- 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; diff -r 78943ac46f6d -r 7463251e7273 src/Pure/ProofGeneral/ROOT.ML --- 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 *) diff -r 78943ac46f6d -r 7463251e7273 src/Pure/ProofGeneral/preferences.ML --- 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" diff -r 78943ac46f6d -r 7463251e7273 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r 78943ac46f6d -r 7463251e7273 src/Pure/pure_setup.ML --- 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;