src/FOLP/simp.ML
changeset 59170 de18f8b1a5a2
parent 58963 26bf09b95dda
child 59498 50b60f501b05
     1.1 --- a/src/FOLP/simp.ML	Sun Dec 21 19:14:16 2014 +0100
     1.2 +++ b/src/FOLP/simp.ML	Sun Dec 21 22:49:17 2014 +0100
     1.3 @@ -221,8 +221,13 @@
     1.4  
     1.5  fun normed_rews congs =
     1.6    let val add_norms = add_norm_tags congs in
     1.7 -    fn thm => Variable.tradeT
     1.8 -      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm]
     1.9 +    fn thm =>
    1.10 +      let
    1.11 +        val ctxt =
    1.12 +          Thm.theory_of_thm thm
    1.13 +          |> Proof_Context.init_global
    1.14 +          |> Variable.declare_thm thm;
    1.15 +      in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end
    1.16    end;
    1.17  
    1.18  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];