# HG changeset patch # User wenzelm # Date 1272664417 -7200 # Node ID d5d6111761a6189a01e67319ef4c59d771243e74 # Parent 0cbcdfd9e527118c65c9fbfd1df156ae5e9e5699 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing; diff -r 0cbcdfd9e527 -r d5d6111761a6 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Apr 30 23:43:09 2010 +0200 +++ b/src/FOLP/simp.ML Fri Apr 30 23:53:37 2010 +0200 @@ -222,7 +222,7 @@ fun normed_rews congs = let val add_norms = add_norm_tags congs in fn thm => Variable.tradeT - (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm] + (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm] end; fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Fri Apr 30 23:43:09 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Apr 30 23:53:37 2010 +0200 @@ -152,7 +152,8 @@ in case map_filter (fn th'' => SOME (th'', singleton - (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') + (Variable.trade (K (fn [th'''] => [th''' RS th'])) + (Variable.global_thm_context th'')) th'') handle THM _ => NONE) thms of [] => NONE | thps => diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Apr 30 23:43:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Apr 30 23:53:37 2010 +0200 @@ -355,7 +355,7 @@ if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then [] else let - val ctxt0 = Variable.thm_context th + val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt1) = to_nnf th ctxt0 val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end @@ -408,7 +408,7 @@ local fun skolem_def (name, th) thy = - let val ctxt0 = Variable.thm_context th in + let val ctxt0 = Variable.global_thm_context th in (case try (to_nnf th) ctxt0 of NONE => (NONE, thy) | SOME (nnfth, ctxt1) => diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Apr 30 23:43:09 2010 +0200 +++ b/src/HOL/Tools/meson.ML Fri Apr 30 23:53:37 2010 +0200 @@ -555,7 +555,7 @@ skolemize_nnf_list ctxt ths); fun add_clauses th cls = - let val ctxt0 = Variable.thm_context th + let val ctxt0 = Variable.global_thm_context th val (cnfs, ctxt) = make_cnf [] th ctxt0 in Variable.export ctxt ctxt0 cnfs @ cls end; diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Apr 30 23:43:09 2010 +0200 +++ b/src/HOL/Tools/simpdata.ML Fri Apr 30 23:53:37 2010 +0200 @@ -95,7 +95,7 @@ fun res th = map (fn rl => th RS rl); (*exception THM*) fun res_fixed rls = if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls - else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm]; + else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm]; in case concl_of thm of Const (@{const_name Trueprop}, _) $ p => (case head_of p diff -r 0cbcdfd9e527 -r d5d6111761a6 src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Apr 30 23:43:09 2010 +0200 +++ b/src/Pure/variable.ML Fri Apr 30 23:53:37 2010 +0200 @@ -28,7 +28,7 @@ val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context - val thm_context: thm -> Proof.context + val global_thm_context: thm -> Proof.context val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term option -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term @@ -235,7 +235,7 @@ val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); val declare_thm = Thm.fold_terms declare_internal; -fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); +fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); (* renaming term/type frees *)