src/HOL/Tools/refute.ML

     (* TODO: it is currently not possible to specify a size for a type    *)
     (*       whose name is one of the other parameters (e.g. 'maxvars')   *)
     (* (string * int) list *)
     val sizes     = map_filter
       (fn (name, value) => Option.map (pair name) (Int.fromString value))
-      (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
+      (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
         andalso name<>"maxvars" andalso name<>"maxtime"
         andalso name<>"satsolver") allparams)
   in
     {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
       maxtime=maxtime, satsolver=satsolver, expect=expect}

         SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
       else
         (* continue search *)
         next max (len+1) (sum+x1) (x2::xs)
     (* only consider those types for which the size is not fixed *)
-    val mutables = List.filter
-      (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
+    val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
     (* subtract 'minsize' from every size (will be added again at the end) *)
     val diffs = map (fn (_, n) => n-minsize) mutables
   in
     case next (maxsize-minsize) 0 0 diffs of
       SOME diffs' =>

                         val (c, args) = get_cargs idx elem
                         (* find the indices of the constructor's /recursive/ *)
                         (* arguments                                         *)
                         val (_, _, constrs) = the (AList.lookup (op =) descr idx)
                         val (_, dtyps)      = List.nth (constrs, c)
-                        val rec_dtyps_args  = List.filter
+                        val rec_dtyps_args  = filter
                           (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
                         (* map those indices to interpretations *)
                         val rec_dtyps_intrs = map (fn (dtyp, arg) =>
                           let
                             val dT     = typ_of_dtyp descr typ_assoc dtyp