# HG changeset patch
# User huffman
# Date 1287089187 25200
# Node ID 575d3aa1f3c5d597f3d5289c1133961ee0af7ac8
# Parent  2eff1cbc1ccb2901db7f846ada7f74fe37034162
include iso_info as part of constr_info type

diff -r 2eff1cbc1ccb -r 575d3aa1f3c5 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:28:31 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:46:27 2010 -0700
@@ -9,6 +9,7 @@
 sig
   type constr_info =
     {
+      iso_info : Domain_Take_Proofs.iso_info,
       con_consts : term list,
       con_betas : thm list,
       nchotomy : thm,
@@ -44,6 +45,7 @@
 
 type constr_info =
   {
+    iso_info : Domain_Take_Proofs.iso_info,
     con_consts : term list,
     con_betas : thm list,
     nchotomy : thm,
@@ -958,7 +960,9 @@
       end;
 
     val result =
-      { con_consts = con_consts,
+      {
+        iso_info = iso_info,
+        con_consts = con_consts,
         con_betas = con_betas,
         nchotomy = nchotomy,
         exhaust = exhaust,
@@ -971,7 +975,8 @@
         cases = cases,
         sel_rews = sel_thms,
         dis_rews = dis_thms,
-        match_rews = match_thms };
+        match_rews = match_thms
+      };
   in
     (result, thy)
   end;
diff -r 2eff1cbc1ccb -r 575d3aa1f3c5 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:28:31 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:46:27 2010 -0700
@@ -198,7 +198,7 @@
     val (take_rews, theorems_thy) =
         thy
           |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
-              (dbinds ~~ map snd eqs') iso_infos take_info constr_infos;
+              (dbinds ~~ map snd eqs') take_info constr_infos;
   in
     theorems_thy
   end;
diff -r 2eff1cbc1ccb -r 575d3aa1f3c5 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
@@ -12,7 +12,6 @@
   val comp_theorems :
       binding * Domain_Library.eq list ->
       (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
-      Domain_Take_Proofs.iso_info list ->
       Domain_Take_Proofs.take_induct_info ->
       Domain_Constructors.constr_info list ->
       theory -> thm list * theory
@@ -99,7 +98,6 @@
 
 fun take_theorems
     (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
-    (iso_infos : Domain_Take_Proofs.iso_info list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (constr_infos : Domain_Constructors.constr_info list)
     (thy : theory) : thm list list * theory =
@@ -113,7 +111,7 @@
   val n' = @{const Suc} $ n;
 
   local
-    val newTs = map #absT iso_infos;
+    val newTs = map (#absT o #iso_info) constr_infos;
     val subs = newTs ~~ map (fn t => t $ n) take_consts;
     fun is_ID (Const (c, _)) = (c = @{const_name ID})
       | is_ID _              = false;
@@ -124,9 +122,9 @@
   end
 
   fun prove_take_apps
-      ((((dbind, spec), iso_info), take_const), constr_info) thy =
+      (((dbind, spec), take_const), constr_info) thy =
     let
-      val {con_consts, con_betas, ...} = constr_info;
+      val {iso_info, con_consts, con_betas, ...} = constr_info;
       val {abs_inverse, ...} = iso_info;
       fun prove_take_app (con_const : term) (bind, args, mx) =
         let
@@ -151,7 +149,7 @@
     end;
 in
   fold_map prove_take_apps
-    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
+    (specs ~~ take_consts ~~ constr_infos) thy
 end;
 
 (* ----- general proofs ----------------------------------------------------- *)
@@ -510,7 +508,6 @@
 fun comp_theorems
     (comp_dbind : binding, eqs : eq list)
     (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
-    (iso_infos : Domain_Take_Proofs.iso_info list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (constr_infos : Domain_Constructors.constr_info list)
     (thy : theory) =
@@ -539,7 +536,7 @@
 (* theorems about take *)
 
 val (take_rewss, thy) =
-    take_theorems specs iso_infos take_info constr_infos thy;
+    take_theorems specs take_info constr_infos thy;
 
 val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;