src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32952 aeb1e44fbc19
parent 32740 9dd0a2f83429
child 32957 675c0c7e6a37
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4      let
     1.5        fun def_of_sel sel = ga (sel^"_def") dname;
     1.6        fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
     1.7 -      fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
     1.8 +      fun defs_of_con (_, args) = map_filter def_of_arg args;
     1.9      in
    1.10        maps defs_of_con cons
    1.11      end;
    1.12 @@ -434,7 +434,7 @@
    1.13        (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
    1.14  
    1.15    fun sel_strict (_, args) =
    1.16 -    List.mapPartial (Option.map one_sel o sel_of) args;
    1.17 +    map_filter (Option.map one_sel o sel_of) args;
    1.18  in
    1.19    val _ = trace " Proving sel_stricts...";
    1.20    val sel_stricts = maps sel_strict cons;
    1.21 @@ -492,7 +492,7 @@
    1.22    val _ = trace " Proving sel_defins...";
    1.23    val sel_defins =
    1.24      if length cons = 1
    1.25 -    then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
    1.26 +    then map_filter (fn arg => Option.map sel_defin (sel_of arg))
    1.27                   (filter_out is_lazy (snd (hd cons)))
    1.28      else [];
    1.29  end;