src/FOLP/simp.ML
changeset 19876 11d447d5d68c
parent 19805 854404b8f738
child 19925 3f9341831812
     1.1 --- a/src/FOLP/simp.ML	Tue Jun 13 23:41:37 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Jun 13 23:41:39 2006 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4  
     1.5  fun normed_rews congs =
     1.6    let val add_norms = add_norm_tags congs;
     1.7 -  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
     1.8 +  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
     1.9    end;
    1.10  
    1.11  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];