src/HOLCF/domain/theorems.ML
 changeset 16842 5979c46853d1 parent 16778 2162c0de4673 child 17465 93fc1211603f
```     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:23 2005 +0200
1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:24 2005 +0200
1.3 @@ -6,6 +6,7 @@
1.4  Proof generator for domain section.
1.5  *)
1.6
1.7 +val HOLCF_ss = simpset();
1.8
1.9  structure Domain_Theorems = struct
1.10
1.11 @@ -233,7 +234,7 @@
1.12                                                    (List.nth(vns,n))] else [])
1.13                       @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
1.14  in List.concat(map  (fn (c,args) =>
1.15 -     List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
1.16 +     List.concat(List.mapPartial I (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
1.17  val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==>
1.18                          defined(%%:sel`%x_name)) [
1.19                                  rtac casedist 1,
1.20 @@ -442,7 +443,7 @@
1.21      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
1.22      fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (warning
1.23          ("domain "^List.nth(dnames,n)^" is empty!"); true) else false;
1.24 -    fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
1.25 +    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
1.26
1.27    in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
1.28       val is_emptys = map warn n__eqs;
```