src/ZF/Tools/induct_tacs.ML

 
 fun find_tname var Bi =
   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
              (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
-      val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
+      val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
           (#2 (strip_context Bi))
   in case assoc (pairs, var) of
        NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
      | SOME t => t
   end;

           |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
           |> DatatypesData.put
               (Symtab.update
                ((big_rec_name, dt_info), DatatypesData.get thy))
           |> ConstructorsData.put
-               (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+               (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
           |> Theory.parent_path
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let