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;