--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Oct 14 09:44:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Oct 14 10:16:46 2010 -0700
@@ -639,9 +639,8 @@
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(dbinds ~~ iso_infos) thy;
- val { take_consts, take_defs, chain_take_thms, take_0_thms,
- take_Suc_thms, deflation_take_thms,
- finite_consts, finite_defs } = take_info;
+ val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} =
+ take_info;
(* least-upper-bound lemma for take functions *)
val lub_take_lemma =
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Oct 14 09:44:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Oct 14 10:16:46 2010 -0700
@@ -24,6 +24,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list
}
@@ -35,6 +36,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list,
lub_take_thms : thm list,
@@ -80,6 +82,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list
};
@@ -92,6 +95,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list,
lub_take_thms : thm list,
@@ -429,6 +433,7 @@
take_0_thms = take_0_thms,
take_Suc_thms = take_Suc_thms,
deflation_take_thms = deflation_take_thms,
+ take_strict_thms = take_strict_thms,
finite_consts = finite_consts,
finite_defs = finite_defs
};
@@ -593,6 +598,7 @@
take_0_thms = #take_0_thms take_info,
take_Suc_thms = #take_Suc_thms take_info,
deflation_take_thms = #deflation_take_thms take_info,
+ take_strict_thms = #take_strict_thms take_info,
finite_consts = #finite_consts take_info,
finite_defs = #finite_defs take_info,
lub_take_thms = lub_take_thms,