# HG changeset patch
# User wenzelm
# Date 1407611022 -7200
# Node ID b510819d58eed3eaf1fcd23a61d55b296b58a933
# Parent  d02f0d44764846a0da032c5eb841a124ba473848
tuned;

diff -r d02f0d447648 -r b510819d58ee src/HOL/Library/refute.ML
--- 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
diff -r d02f0d447648 -r b510819d58ee src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Aug 09 07:59:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Aug 09 21:03:42 2014 +0200
@@ -263,7 +263,7 @@
             map (do_term NONE) us)
         else if not (null us) then
           let
-            val args = List.map (do_term NONE) us
+            val args = map (do_term NONE) us
             val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T)
             val func = do_term opt_T' (ATerm ((s, tys), []))
           in foldl1 (op $) (func :: args) end