src/HOL/Nominal/nominal_induct.ML

         val P :: x :: ys = vars;
         val zs = Library.drop (m - n - 2, ys);
       in
         (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
         (x, tuple (map Free avoiding)) ::
-        List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
+        map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
       end;
      val substs =
-       map2 subst insts concls |> List.concat |> distinct (op =)
+       map2 subst insts concls |> flat |> distinct (op =)
        |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;
 

     fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
   in
     (fn i => fn st =>
       rules
       |> inst_mutual_rule ctxt insts avoiding
-      |> RuleCases.consume (List.concat defs) facts
+      |> RuleCases.consume (flat defs) facts
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
             (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
               THEN' Induct.fix_tac defs_ctxt