# HG changeset patch
# User huffman
# Date 1265672941 28800
# Node ID acbc346e53105ae8b461f426b55ba964e997cde6
# Parent  d0cc1650b378cd37e8382bb574667043629ceeee
correct definedness side conditions for copy_apps and take_apps

diff -r d0cc1650b378 -r acbc346e5310 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 11:14:12 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 15:49:01 2010 -0800
@@ -610,6 +610,9 @@
                  (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
           else (%# arg);
       val rhs = con_app2 con one_rhs args;
+      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
+      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
+      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
       val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
       val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
@@ -736,7 +739,6 @@
       val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU);
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
-  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts @ con_rews) 1;
   val _ = trace " Proving take_apps...";
   fun one_take_app dn (con, args) =
     let
@@ -748,12 +750,12 @@
           else (%# arg);
       val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
       val rhs = con_app2 con one_rhs args;
-      val goal = mk_trp (lhs === rhs);
-      fun tacs ctxt =
-        map (c_UU_tac ctxt) (nonlazy_rec args) @ [
-        rewrite_goals_tac copy_take_defs,
-        asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
-    in pg [] goal tacs end;
+      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
+      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
+      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
+      val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
+      val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
+    in pg copy_take_defs goal (K tacs) end;
   fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
   val take_apps = maps one_take_apps eqs;
 in