src/Provers/splitter.ML

--- a/src/Provers/splitter.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/Provers/splitter.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -192,7 +192,7 @@
   if n > length ts then []
   else let val lev = length apsns
            val lbnos = fold add_lbnos (Library.take (n, ts)) []
-           val flbnos = List.filter (fn i => i < lev) lbnos
+           val flbnos = filter (fn i => i < lev) lbnos
            val tt = incr_boundvars (~lev) t
        in if null flbnos then
             if T = T' then [(thm,[],pos,TB,tt)] else []