--- a/src/FOLP/simp.ML Sun Dec 21 19:14:16 2014 +0100
+++ b/src/FOLP/simp.ML Sun Dec 21 22:49:17 2014 +0100
@@ -221,8 +221,13 @@
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.global_thm_context thm) [thm]
+ fn thm =>
+ let
+ val ctxt =
+ Thm.theory_of_thm thm
+ |> Proof_Context.init_global
+ |> Variable.declare_thm thm;
+ in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end
end;
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
--- a/src/Pure/variable.ML Sun Dec 21 19:14:16 2014 +0100
+++ b/src/Pure/variable.ML Sun Dec 21 22:49:17 2014 +0100
@@ -25,7 +25,6 @@
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 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
@@ -269,7 +268,6 @@
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th));
(* renaming term/type frees *)