diff -r dd02201d95b6 -r 63f8121c6585 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 01 16:36:25 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 01 16:58:16 2010 -0800
@@ -463,6 +463,18 @@
     val (take_strict_thms, thy) =
       fold_map prove_take_strict (take_consts ~~ dnames) thy;
 
+    (* prove take/take rules *)
+    fun prove_take_take ((chain_take, deflation_take), dname) thy =
+      let
+        val take_take_thm =
+            @{thm deflation_chain_min} OF [chain_take, deflation_take];
+      in
+        add_qualified_thm "take_take" (dname, take_take_thm) thy
+      end;
+    val (take_take_thms, thy) =
+      fold_map prove_take_take
+        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+
     val result =
       {
         take_consts = take_consts,