src/HOLCF/Tools/Domain/domain_axioms.ML

   val axiomatize_lub_take :
       binding * term -> theory -> thm * theory
 
   val add_axioms :
       (binding * (typ * typ)) list -> theory ->
-      Domain_Take_Proofs.iso_info list * theory
+      (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_induct_info) * theory
 end;
 
 
 structure Domain_Axioms : DOMAIN_AXIOMS =
 struct

     val (take_info2, thy) =
         Domain_Take_Proofs.add_lub_take_theorems
           (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
 
   in
-    (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
+    ((iso_infos, take_info2), thy) (* TODO: also return take_info, lub_take_thms *)
   end;
 
 end; (* struct *)