| 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