# HG changeset patch
# User huffman
# Date 1267552490 28800
# Node ID d1ef88d7de5a2d38e1eb112999f44a3b34494d41
# Parent  6acef0aea07d72a6ab8b1f8854cd3add22842c40
remove dead code

diff -r 6acef0aea07d -r d1ef88d7de5a src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:53:18 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 09:54:50 2010 -0800
@@ -95,10 +95,6 @@
   InductTacs.case_tac ctxt (v^"=UU") i THEN
   asm_simp_tac (HOLCF_ss addsimps rews) i;
 
-val chain_tac =
-  REPEAT_DETERM o resolve_tac 
-    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
-
 (* ----- general proofs ----------------------------------------------------- *)
 
 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
@@ -171,8 +167,6 @@
 
 val pg = pg' thy;
 
-val dc_copy = %%:(dname^"_copy");
-
 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
@@ -195,10 +189,6 @@
           else (%# arg);
       val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
       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 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;