--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 14:33:34 2010 -0800
@@ -602,8 +602,9 @@
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(dom_binds ~~ iso_infos) thy;
- val {take_consts, take_defs, chain_take_thms, take_0_thms,
- take_Suc_thms, deflation_take_thms} = take_info;
+ val { take_consts, take_defs, chain_take_thms, take_0_thms,
+ take_Suc_thms, deflation_take_thms,
+ finite_consts, finite_defs } = take_info;
(* least-upper-bound lemma for take functions *)
val lub_take_lemma =