tuned;
authorwenzelm
Sat Aug 09 21:03:42 2014 +0200 (2014-08-09)
changeset 57820b510819d58ee
parent 57819 d02f0d447648
child 57881 37920df63ab9
tuned;
src/HOL/Library/refute.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
     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
     2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Aug 09 07:59:15 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Aug 09 21:03:42 2014 +0200
     2.3 @@ -263,7 +263,7 @@
     2.4              map (do_term NONE) us)
     2.5          else if not (null us) then
     2.6            let
     2.7 -            val args = List.map (do_term NONE) us
     2.8 +            val args = map (do_term NONE) us
     2.9              val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T)
    2.10              val func = do_term opt_T' (ATerm ((s, tys), []))
    2.11            in foldl1 (op $) (func :: args) end