src/Pure/Proof/extraction.ML

                       corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
 
                     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';
                     val c = Const (cname, T);
                     val u = mkabs (list_comb (c, args')) args;