src/FOLP/simp.ML
changeset 21287 a713ae348e8a
parent 21078 101aefd61aac
child 22360 26ead7ed4f4b
     1.1 --- a/src/FOLP/simp.ML	Fri Nov 10 07:44:47 2006 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Nov 10 10:42:25 2006 +0100
     1.3 @@ -222,8 +222,8 @@
     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 (Variable.thm_context thm)
     1.8 -      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
     1.9 +    fn thm => Variable.tradeT
    1.10 +      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
    1.11    end;
    1.12  
    1.13  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];