# HG changeset patch
# User huffman
# Date 1268062631 28800
# Node ID 5dd352a854649390b3de78cef0621fee2c40325c
# Parent  64fff18d7f08cd03cb4d7b23f47c652ef9390a6d
add type take_info

diff -r 64fff18d7f08 -r 5dd352a85464 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 07:22:30 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 07:37:11 2010 -0800
@@ -16,9 +16,7 @@
       abs_inverse : thm,
       rep_inverse : thm
     }
-
-  val define_take_functions :
-    (binding * iso_info) list -> theory ->
+  type take_info =
     { take_consts : term list,
       take_defs : thm list,
       chain_take_thms : thm list,
@@ -27,7 +25,9 @@
       deflation_take_thms : thm list,
       finite_consts : term list,
       finite_defs : thm list
-    } * theory
+    }
+  val define_take_functions :
+    (binding * iso_info) list -> theory -> take_info * theory
 
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
@@ -52,6 +52,17 @@
     rep_inverse : thm
   };
 
+type take_info =
+  { take_consts : term list,
+    take_defs : thm list,
+    chain_take_thms : thm list,
+    take_0_thms : thm list,
+    take_Suc_thms : thm list,
+    deflation_take_thms : thm list,
+    finite_consts : term list,
+    finite_defs : thm list
+  };
+
 val beta_ss =
   HOL_basic_ss
     addsimps simp_thms