add rule deflation_ID to proof script for take + constructor rules

--- a/src/HOLCF/Domain.thy	Thu Apr 15 21:24:00 2010 +0200
+++ b/src/HOLCF/Domain.thy	Thu Apr 15 18:21:05 2010 -0700
@@ -149,8 +149,8 @@
   cfcomp2 sfst_defined_iff ssnd_defined_iff
 
 lemmas take_con_rules =
-  ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
-  sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+  ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
+  deflation_strict deflation_ID ID1 cfcomp2
 
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Apr 15 21:24:00 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Apr 15 18:21:05 2010 -0700
@@ -184,8 +184,7 @@
       val rhs = con_app2 con one_rhs args;
       val goal = mk_trp (lhs === rhs);
       val rules =
-          [ax_abs_iso]
-          @ @{thms take_con_rules ID1 cfcomp2 deflation_strict}
+          [ax_abs_iso] @ @{thms take_con_rules}
           @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
       val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
     in pg con_appls goal (K tacs) end;