src/HOL/Nominal/nominal_inductive.ML
changeset 32952 aeb1e44fbc19
parent 32202 443d5cfaba1b
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4        | lift_prem t = t;
     1.5  
     1.6      fun mk_distinct [] = []
     1.7 -      | mk_distinct ((x, T) :: xs) = List.mapPartial (fn (y, U) =>
     1.8 +      | mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) =>
     1.9            if T = U then SOME (HOLogic.mk_Trueprop
    1.10              (HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
    1.11            else NONE) xs @ mk_distinct xs;
    1.12 @@ -263,7 +263,7 @@
    1.13  
    1.14      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    1.15        map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    1.16 -          (List.mapPartial (fn prem =>
    1.17 +          (map_filter (fn prem =>
    1.18               if null (preds_of ps prem) then SOME prem
    1.19               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    1.20          (mk_distinct bvars @
    1.21 @@ -359,7 +359,7 @@
    1.22                             (etac conjunct1 1) monos NONE th,
    1.23                           mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    1.24                             (inst_conj_all_tac (length pis'')) monos (SOME t) th))))
    1.25 -                      (gprems ~~ oprems)) |>> List.mapPartial I;
    1.26 +                      (gprems ~~ oprems)) |>> map_filter I;
    1.27                   val vc_compat_ths' = map (fn th =>
    1.28                     let
    1.29                       val th' = first_order_mrs gprems1 th;