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;