--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 11:58:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 12:21:07 2010 -0800
@@ -17,6 +17,7 @@
val add_axioms :
(binding * (typ * typ)) list -> theory ->
(Domain_Take_Proofs.iso_info list
+ * Domain_Take_Proofs.take_info
* Domain_Take_Proofs.take_induct_info) * theory
end;
@@ -127,7 +128,7 @@
(map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
in
- ((iso_infos, take_info2), thy) (* TODO: also return take_info, lub_take_thms *)
+ ((iso_infos, take_info, take_info2), thy)
end;
end; (* struct *)