fix proof script for take_apps so it works with indirect recursion

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 16:07:48 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 16:25:59 2010 -0800
@@ -176,8 +176,9 @@
 local
   fun dc_take dn = %%:(dn^"_take");
   val dnames = map (fst o fst) eqs;
-  fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
-  val axs_take_strict = map get_take_strict dnames;
+  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
+  fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
+  val axs_deflation_take = map get_deflation_take dnames;
 
   fun one_take_app (con, args) =
     let
@@ -191,7 +192,9 @@
       val rhs = con_app2 con one_rhs args;
       val goal = mk_trp (lhs === rhs);
       val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
-      val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
+      val rules2 =
+          @{thms take_con_rules ID1 deflation_strict}
+          @ deflation_thms @ axs_deflation_take;
       val tacs =
           [simp_tac (HOL_basic_ss addsimps rules) 1,
            asm_simp_tac (HOL_basic_ss addsimps rules2) 1];