# HG changeset patch
# User huffman
# Date 1287074680 25200
# Node ID 7469b323e2601c3af91266efc4bec3ac0c7a5963
# Parent  9db8fb58fddc5bc1069cc2d017fef099850b449f
add record type synonym 'constr_info'

diff -r 9db8fb58fddc -r 7469b323e260 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 09:34:00 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 09:44:40 2010 -0700
@@ -7,26 +7,29 @@
 
 signature DOMAIN_CONSTRUCTORS =
 sig
+  type constr_info =
+    {
+      con_consts : term list,
+      con_betas : thm list,
+      nchotomy : thm,
+      exhaust : thm,
+      compacts : thm list,
+      con_rews : thm list,
+      inverts : thm list,
+      injects : thm list,
+      dist_les : thm list,
+      dist_eqs : thm list,
+      cases : thm list,
+      sel_rews : thm list,
+      dis_rews : thm list,
+      match_rews : thm list
+    }
   val add_domain_constructors :
       binding
       -> (binding * (bool * binding option * typ) list * mixfix) list
       -> Domain_Take_Proofs.iso_info
       -> theory
-      -> { con_consts : term list,
-           con_betas : thm list,
-           nchotomy : thm,
-           exhaust : thm,
-           compacts : thm list,
-           con_rews : thm list,
-           inverts : thm list,
-           injects : thm list,
-           dist_les : thm list,
-           dist_eqs : thm list,
-           cases : thm list,
-           sel_rews : thm list,
-           dis_rews : thm list,
-           match_rews : thm list
-         } * theory;
+      -> constr_info * theory;
 end;
 
 
@@ -39,6 +42,24 @@
 infix -->>;
 infix 9 `;
 
+type constr_info =
+  {
+    con_consts : term list,
+    con_betas : thm list,
+    nchotomy : thm,
+    exhaust : thm,
+    compacts : thm list,
+    con_rews : thm list,
+    inverts : thm list,
+    injects : thm list,
+    dist_les : thm list,
+    dist_eqs : thm list,
+    cases : thm list,
+    sel_rews : thm list,
+    dis_rews : thm list,
+    match_rews : thm list
+  }
+
 (************************** miscellaneous functions ***************************)
 
 val simple_ss = HOL_basic_ss addsimps simp_thms;
diff -r 9db8fb58fddc -r 7469b323e260 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:34:00 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:44:40 2010 -0700
@@ -106,7 +106,7 @@
     (((dname, _), cons) : eq, eqs : eq list)
     (iso_info : Domain_Take_Proofs.iso_info)
     (take_info : Domain_Take_Proofs.take_induct_info)
-    (result)
+    (result : Domain_Constructors.constr_info)
     (thy : theory) =
 let
   val map_tab = Domain_Take_Proofs.get_map_tab thy;