src/HOLCF/Tools/Domain/domain_theorems.ML

   val axs_pat_def = map (get_def pat_name) cons;
   val axs_sel_def =
     let
       fun def_of_sel sel = ga (sel^"_def") dname;
       fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
-      fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
+      fun defs_of_con (_, args) = map_filter def_of_arg args;
     in
       maps defs_of_con cons
     end;
   val ax_copy_def = ga "copy_def" dname;
 end; (* local *)

   fun one_sel sel =
     pg axs_sel_def (mk_trp (strict (%%:sel)))
       (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
 
   fun sel_strict (_, args) =
-    List.mapPartial (Option.map one_sel o sel_of) args;
+    map_filter (Option.map one_sel o sel_of) args;
 in
   val _ = trace " Proving sel_stricts...";
   val sel_stricts = maps sel_strict cons;
 end;
 

     in pg [] goal (K tacs) end;
 in
   val _ = trace " Proving sel_defins...";
   val sel_defins =
     if length cons = 1
-    then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
+    then map_filter (fn arg => Option.map sel_defin (sel_of arg))
                  (filter_out is_lazy (snd (hd cons)))
     else [];
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;