src/HOL/Library/refute.ML
changeset 57820 b510819d58ee
parent 56853 a265e41cc33b
child 58109 6d4695335d41
     1.1 --- a/src/HOL/Library/refute.ML	Sat Aug 09 07:59:15 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Sat Aug 09 21:03:42 2014 +0200
     1.3 @@ -2909,7 +2909,7 @@
     1.4            Node xs => xs
     1.5          | _       => raise REFUTE ("set_printer",
     1.6            "interpretation for set type is a leaf"))
     1.7 -      val elements = List.mapPartial (fn (arg, result) =>
     1.8 +      val elements = map_filter (fn (arg, result) =>
     1.9          case result of
    1.10            Leaf [fmTrue, (* fmFalse *) _] =>
    1.11            if Prop_Logic.eval assignment fmTrue then