src/FOLP/simp.ML
changeset 36603 d5d6111761a6
parent 35021 c839a4c670c6
child 36692 54b64d4ad524
     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];