1.1 --- a/src/FOLP/simp.ML	Fri Apr 30 23:43:09 2010 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri Apr 30 23:53:37 2010 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4  fun normed_rews congs =
     1.5    let val add_norms = add_norm_tags congs in
     1.6      fn thm => Variable.tradeT
     1.7 -      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
     1.8 +      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm]
     1.9    end;
    1.10  
    1.11  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];

     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:43:09 2010 +0200
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:53:37 2010 +0200
     2.3 @@ -152,7 +152,8 @@
     2.4        in
     2.5          case map_filter (fn th'' =>
     2.6              SOME (th'', singleton
     2.7 -              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
     2.8 +              (Variable.trade (K (fn [th'''] => [th''' RS th']))
     2.9 +                (Variable.global_thm_context th'')) th'')
    2.10            handle THM _ => NONE) thms of
    2.11              [] => NONE
    2.12            | thps =>

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Apr 30 23:43:09 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Apr 30 23:53:37 2010 +0200
     3.3 @@ -355,7 +355,7 @@
     3.4    if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
     3.5    else
     3.6      let
     3.7 -      val ctxt0 = Variable.thm_context th
     3.8 +      val ctxt0 = Variable.global_thm_context th
     3.9        val (nnfth, ctxt1) = to_nnf th ctxt0
    3.10        val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
    3.11      in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
    3.12 @@ -408,7 +408,7 @@
    3.13  local
    3.14  
    3.15  fun skolem_def (name, th) thy =
    3.16 -  let val ctxt0 = Variable.thm_context th in
    3.17 +  let val ctxt0 = Variable.global_thm_context th in
    3.18      (case try (to_nnf th) ctxt0 of
    3.19        NONE => (NONE, thy)
    3.20      | SOME (nnfth, ctxt1) =>

     4.1 --- a/src/HOL/Tools/meson.ML	Fri Apr 30 23:43:09 2010 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Fri Apr 30 23:53:37 2010 +0200
     4.3 @@ -555,7 +555,7 @@
     4.4          skolemize_nnf_list ctxt ths);
     4.5  
     4.6  fun add_clauses th cls =
     4.7 -  let val ctxt0 = Variable.thm_context th
     4.8 +  let val ctxt0 = Variable.global_thm_context th
     4.9        val (cnfs, ctxt) = make_cnf [] th ctxt0
    4.10    in Variable.export ctxt ctxt0 cnfs @ cls end;
    4.11  

     5.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 30 23:43:09 2010 +0200
     5.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 30 23:53:37 2010 +0200
     5.3 @@ -95,7 +95,7 @@
     5.4          fun res th = map (fn rl => th RS rl);   (*exception THM*)
     5.5          fun res_fixed rls =
     5.6            if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
     5.7 -          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
     5.8 +          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
     5.9        in
    5.10          case concl_of thm
    5.11            of Const (@{const_name Trueprop}, _) $ p => (case head_of p

     6.1 --- a/src/Pure/variable.ML	Fri Apr 30 23:43:09 2010 +0200
     6.2 +++ b/src/Pure/variable.ML	Fri Apr 30 23:53:37 2010 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4    val declare_typ: typ -> Proof.context -> Proof.context
     6.5    val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
     6.6    val declare_thm: thm -> Proof.context -> Proof.context
     6.7 -  val thm_context: thm -> Proof.context
     6.8 +  val global_thm_context: thm -> Proof.context
     6.9    val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
    6.10    val bind_term: indexname * term option -> Proof.context -> Proof.context
    6.11    val expand_binds: Proof.context -> term -> term
    6.12 @@ -235,7 +235,7 @@
    6.13  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
    6.14  
    6.15  val declare_thm = Thm.fold_terms declare_internal;
    6.16 -fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    6.17 +fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    6.18  
    6.19  
    6.20  (* renaming term/type frees *)