# HG changeset patch
# User wenzelm
# Date 1419198557 -3600
# Node ID de18f8b1a5a2ff85fe432403b8c13bf28738ba8f
# Parent  ddc948e4ed098174961def5b6783ba9fa30bfe34
tuned signature;

diff -r ddc948e4ed09 -r de18f8b1a5a2 src/FOLP/simp.ML
--- 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];
diff -r ddc948e4ed09 -r de18f8b1a5a2 src/Pure/variable.ML
--- 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 *)