src/FOLP/simp.ML

--- a/src/FOLP/simp.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/FOLP/simp.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -215,7 +215,7 @@
 
 fun add_norm_tags congs =
     let val ccs = map cong_const congs
-        val new_asms = List.filter (exists not o #2)
+        val new_asms = filter (exists not o #2)
                 (ccs ~~ (map (map atomic o prems_of) congs));
     in add_norms(congs,ccs,new_asms) end;