# HG changeset patch
# User huffman
# Date 1268077709 28800
# Node ID b6273135281282e67e968dd42333a192d3774883
# Parent  e8e4af6da8192a724a533fe180fa784140ce9798
add type take_induct_info

diff -r e8e4af6da819 -r b62731352812 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 11:34:53 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 11:48:29 2010 -0800
@@ -26,12 +26,19 @@
       finite_consts : term list,
       finite_defs : thm list
     }
+  type take_induct_info =
+    {
+      reach_thms : thm list,
+      take_lemma_thms : thm list,
+      is_finite : bool,
+      take_induct_thms : thm list
+    }
   val define_take_functions :
     (binding * iso_info) list -> theory -> take_info * theory
 
   val add_lub_take_theorems :
     (binding * iso_info) list -> take_info -> thm list ->
-    theory -> thm list * theory
+    theory -> take_induct_info * theory
 
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
@@ -67,6 +74,14 @@
     finite_defs : thm list
   };
 
+type take_induct_info =
+  {
+    reach_thms : thm list,
+    take_lemma_thms : thm list,
+    is_finite : bool,
+    take_induct_thms : thm list
+  };
+
 val beta_ss =
   HOL_basic_ss
     addsimps simp_thms
@@ -579,7 +594,13 @@
           ((NONE, take_inducts), thy)
         end;
 
-    val result = take_induct_thms;
+    val result =
+      {
+        reach_thms = reach_thms,
+        take_lemma_thms = take_lemma_thms,
+        is_finite = is_finite,
+        take_induct_thms = take_induct_thms
+      };
   in
     (result, thy)
   end;