src/HOLCF/Tools/Domain/domain_theorems.ML
 changeset 32952 aeb1e44fbc19 parent 32740 9dd0a2f83429 child 32957 675c0c7e6a37
```--- 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;```