diff -r 83392f9d303f -r aeb1e44fbc19 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -224,7 +224,7 @@
       | lift_prem t = t;
 
     fun mk_distinct [] = []
-      | mk_distinct ((x, T) :: xs) = List.mapPartial (fn (y, U) =>
+      | mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) =>
           if T = U then SOME (HOLogic.mk_Trueprop
             (HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
           else NONE) xs @ mk_distinct xs;
@@ -263,7 +263,7 @@
 
     val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
       map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
-          (List.mapPartial (fn prem =>
+          (map_filter (fn prem =>
              if null (preds_of ps prem) then SOME prem
              else map_term (split_conj (K o I) names) prem prem) prems, q))))
         (mk_distinct bvars @
@@ -359,7 +359,7 @@
                            (etac conjunct1 1) monos NONE th,
                          mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
                            (inst_conj_all_tac (length pis'')) monos (SOME t) th))))
-                      (gprems ~~ oprems)) |>> List.mapPartial I;
+                      (gprems ~~ oprems)) |>> map_filter I;
                  val vc_compat_ths' = map (fn th =>
                    let
                      val th' = first_order_mrs gprems1 th;