--- 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;