src/HOL/Tools/refute.ML
changeset 33317 b4534348b8fd
parent 33246 46e47aa1558f
child 33339 d41f77196338
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -394,7 +394,7 @@
     1.4      (* (string * int) list *)
     1.5      val sizes     = map_filter
     1.6        (fn (name, value) => Option.map (pair name) (Int.fromString value))
     1.7 -      (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
     1.8 +      (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
     1.9          andalso name<>"maxvars" andalso name<>"maxtime"
    1.10          andalso name<>"satsolver") allparams)
    1.11    in
    1.12 @@ -1070,8 +1070,7 @@
    1.13          (* continue search *)
    1.14          next max (len+1) (sum+x1) (x2::xs)
    1.15      (* only consider those types for which the size is not fixed *)
    1.16 -    val mutables = List.filter
    1.17 -      (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
    1.18 +    val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
    1.19      (* subtract 'minsize' from every size (will be added again at the end) *)
    1.20      val diffs = map (fn (_, n) => n-minsize) mutables
    1.21    in
    1.22 @@ -2552,7 +2551,7 @@
    1.23                          (* arguments                                         *)
    1.24                          val (_, _, constrs) = the (AList.lookup (op =) descr idx)
    1.25                          val (_, dtyps)      = List.nth (constrs, c)
    1.26 -                        val rec_dtyps_args  = List.filter
    1.27 +                        val rec_dtyps_args  = filter
    1.28                            (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
    1.29                          (* map those indices to interpretations *)
    1.30                          val rec_dtyps_intrs = map (fn (dtyp, arg) =>