diff -r 83392f9d303f -r aeb1e44fbc19 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -149,7 +149,7 @@
     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;
@@ -434,7 +434,7 @@
       (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;
@@ -492,7 +492,7 @@
   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;