src/FOLP/simp.ML
changeset 19925 3f9341831812
parent 19876 11d447d5d68c
child 20194 c9dbce9a23a1
     1.1 --- a/src/FOLP/simp.ML	Mon Jun 19 19:56:32 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Mon Jun 19 20:21:30 2006 +0200
     1.3 @@ -221,8 +221,9 @@
     1.4      in add_norms(congs,ccs,new_asms) end;
     1.5  
     1.6  fun normed_rews congs =
     1.7 -  let val add_norms = add_norm_tags congs;
     1.8 -  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
     1.9 +  let val add_norms = add_norm_tags congs in
    1.10 +    fn thm => Variable.tradeT (Variable.thm_context thm)
    1.11 +      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
    1.12    end;
    1.13  
    1.14  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];