src/FOLP/simp.ML
changeset 20951 868120282837
parent 20194 c9dbce9a23a1
child 21078 101aefd61aac
     1.1 --- a/src/FOLP/simp.ML	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4  val delete_thms = foldr delete_thm_warn;
     1.5  
     1.6  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
     1.7 -let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
     1.8 +let val congs' = fold (remove Drule.eq_thm_prop) thms congs
     1.9  in SS{auto_tac=auto_tac, congs= congs',
    1.10        cong_net= delete_thms cong_net (map mk_trans thms),
    1.11        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}