src/HOLCF/Tools/Domain/domain_constructors.ML

 signature DOMAIN_CONSTRUCTORS =
 sig
   val add_domain_constructors :
       string
       -> (binding * (bool * binding option * typ) list * mixfix) list
-      -> Domain_Isomorphism.iso_info
+      -> Domain_Take_Proofs.iso_info
       -> theory
       -> { con_consts : term list,
            con_betas : thm list,
            exhaust : thm,
            casedist : thm,

 (******************************************************************************)
 
 fun add_domain_constructors
     (dname : string)
     (spec : (binding * (bool * binding option * typ) list * mixfix) list)
-    (iso_info : Domain_Isomorphism.iso_info)
+    (iso_info : Domain_Take_Proofs.iso_info)
     (thy : theory) =
   let
 
     (* retrieve facts about rep/abs *)
     val lhsT = #absT iso_info;