src/FOLP/simp.ML
changeset 33317 b4534348b8fd
parent 33245 65232054ffd0
child 33339 d41f77196338
     1.1 --- a/src/FOLP/simp.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  
     1.5  fun add_norm_tags congs =
     1.6      let val ccs = map cong_const congs
     1.7 -        val new_asms = List.filter (exists not o #2)
     1.8 +        val new_asms = filter (exists not o #2)
     1.9                  (ccs ~~ (map (map atomic o prems_of) congs));
    1.10      in add_norms(congs,ccs,new_asms) end;
    1.11