# HG changeset patch
# User huffman
# Date 1287076606 25200
# Node ID 2fda967490810908068534f5cd28ef19450bf352
# Parent  7469b323e2601c3af91266efc4bec3ac0c7a5963
add take_strict_thms field to take_info type

diff -r 7469b323e260 -r 2fda96749081 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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 =
diff -r 7469b323e260 -r 2fda96749081 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- 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,