--- 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
--- 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