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;