# HG changeset patch
# User huffman
# Date 1268078320 28800
# Node ID 0537c34c6067ee9aa5e839c9c16eae008a2c2306
# Parent  b6273135281282e67e968dd42333a192d3774883
pass take_induct_info as an argument to comp_theorems

diff -r b62731352812 -r 0537c34c6067 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 11:48:29 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 11:58:40 2010 -0800
@@ -16,7 +16,8 @@
 
   val add_axioms :
       (binding * (typ * typ)) list -> theory ->
-      Domain_Take_Proofs.iso_info list * theory
+      (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_induct_info) * theory
 end;
 
 
@@ -126,7 +127,7 @@
           (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
 
   in
-    (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
+    ((iso_infos, take_info2), thy) (* TODO: also return take_info, lub_take_thms *)
   end;
 
 end; (* struct *)
diff -r b62731352812 -r 0537c34c6067 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Mar 08 11:48:29 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Mar 08 11:58:40 2010 -0800
@@ -184,7 +184,7 @@
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     val repTs : typ list = map mk_eq_typ eqs';
     val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
-    val (iso_infos, thy) =
+    val ((iso_infos, take_info2), thy) =
         Domain_Axioms.add_axioms dom_eqns thy;
 
     val ((rewss, take_rews), theorems_thy) =
@@ -192,7 +192,7 @@
           |> fold_map (fn ((eq, (x,cs)), info) =>
                 Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
              (eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info2;
   in
     theorems_thy
       |> Sign.add_path (Long_Name.base_name comp_dnam)
@@ -246,7 +246,7 @@
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     
-    val (iso_infos, thy) = thy |>
+    val ((iso_infos, take_info2), thy) = thy |>
       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
@@ -268,7 +268,7 @@
           |> fold_map (fn ((eq, (x,cs)), info) =>
                Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
              (eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info2;
   in
     theorems_thy
       |> Sign.add_path (Long_Name.base_name comp_dnam)
diff -r b62731352812 -r 0537c34c6067 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 11:48:29 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 11:58:40 2010 -0800
@@ -7,8 +7,12 @@
 signature DOMAIN_ISOMORPHISM =
 sig
   val domain_isomorphism :
-    (string list * binding * mixfix * typ * (binding * binding) option) list
-      -> theory -> Domain_Take_Proofs.iso_info list * theory
+      (string list * binding * mixfix * typ
+       * (binding * binding) option) list ->
+      theory ->
+      (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_induct_info) * theory
+
   val domain_isomorphism_cmd :
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
@@ -265,7 +269,8 @@
     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
     (thy: theory)
-    : Domain_Take_Proofs.iso_info list * theory =
+    : (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_induct_info) * theory =
   let
     val _ = Theory.requires thy "Representable" "domain isomorphisms";
 
@@ -649,7 +654,7 @@
         Domain_Take_Proofs.add_lub_take_theorems
           (dom_binds ~~ iso_infos) take_info lub_take_thms thy;
   in
-    (iso_infos, thy)
+    ((iso_infos, take_info2), thy)
   end;
 
 val domain_isomorphism = gen_domain_isomorphism cert_typ;
diff -r b62731352812 -r 0537c34c6067 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 11:48:29 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 11:58:40 2010 -0800
@@ -15,7 +15,11 @@
     -> Domain_Take_Proofs.iso_info
     -> theory -> thm list * theory;
 
-  val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+  val comp_theorems :
+      bstring * Domain_Library.eq list ->
+      Domain_Take_Proofs.take_induct_info ->
+      theory -> thm list * theory
+
   val quiet_mode: bool Unsynchronized.ref;
   val trace_domain: bool Unsynchronized.ref;
 end;
@@ -604,7 +608,10 @@
        |> Sign.parent_path
 end; (* let *)
 
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
+fun comp_theorems
+    (comp_dnam : string, eqs : eq list)
+    (take_induct_info : Domain_Take_Proofs.take_induct_info)
+    (thy : theory) =
 let
 val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
@@ -629,12 +636,8 @@
 
 (* theorems about take *)
 
-local
-  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
-in
-  val take_lemmas = map (ga "take_lemma") dnames;
-  val axs_reach   = map (ga "reach"     ) dnames;
-end;
+val take_lemmas = #take_lemma_thms take_induct_info;
+val axs_reach = #reach_thms take_induct_info;
 
 val take_rews =
     maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;