# HG changeset patch
# User huffman
# Date 1267824797 28800
# Node ID f638444c966793b318be5151b967dfe1ca4c8ed2
# Parent  a76cce4ad3206c45d2f6e416cc306cbc07b2104b
fix proof script so 'domain foo = Foo foo' works

diff -r a76cce4ad320 -r f638444c9667 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 13:27:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 13:33:17 2010 -0800
@@ -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