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