src/HOLCF/Tools/Domain/domain_isomorphism.ML

 *)
 
 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
   val add_type_constructor :
     (string * term * string * thm  * thm * thm * thm) -> theory -> theory

 
 fun gen_domain_isomorphism
     (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";
 
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>

     (* prove additional take theorems *)
     val (take_info2, thy) =
         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;
 val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ;