src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -651,7 +651,7 @@
                     val nt = Envir.beta_norm t;
                     val args = filter_out (fn v => member (op =) rtypes
                       (tname_of (body_type (fastype_of v)))) (vfs_of prop);
-                    val args' = List.filter (fn v => Logic.occs (v, nt)) args;
+                    val args' = filter (fn v => Logic.occs (v, nt)) args;
                     val t' = mkabs nt args';
                     val T = fastype_of t';
                     val cname = extr_name s vs';