# HG changeset patch
# User wenzelm
# Date 1267828318 -3600
# Node ID ad7d2f9cc47dfcd4387adeda8f058960b9a8e235
# Parent  f1429d5df3d2381c63fd07594f2ab4633be4a7af# Parent  f638444c966793b318be5151b967dfe1ca4c8ed2
merged

diff -r f1429d5df3d2 -r ad7d2f9cc47d src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 05 21:29:55 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 05 23:31:58 2010 +0100
@@ -350,7 +350,7 @@
         val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
         val REP_simps = RepData.get thy;
         val tac =
-          simp_tac (HOL_basic_ss addsimps REP_simps) 1
+          rewrite_goals_tac (map mk_meta_eq REP_simps)
           THEN resolve_tac defl_unfold_thms 1;
       in
         Goal.prove_global thy [] [] goal (K tac)
diff -r f1429d5df3d2 -r ad7d2f9cc47d src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 21:29:55 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 23:31:58 2010 +0100
@@ -157,13 +157,11 @@
       val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
       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 deflation_strict}
+      val rules =
+          [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]
+          @ @{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];
+      val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
     in pg con_appls goal (K tacs) end;
   val take_apps = map one_take_app cons;
 in