# 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 *)