src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35590 f638444c9667
parent 35585 555f26f00e47
child 35597 e4331b99b03f
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 13:27:40 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 13:33:17 2010 -0800
     1.3 @@ -157,13 +157,11 @@
     1.4        val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
     1.5        val rhs = con_app2 con one_rhs args;
     1.6        val goal = mk_trp (lhs === rhs);
     1.7 -      val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
     1.8 -      val rules2 =
     1.9 -          @{thms take_con_rules ID1 deflation_strict}
    1.10 +      val rules =
    1.11 +          [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]
    1.12 +          @ @{thms take_con_rules ID1 deflation_strict}
    1.13            @ deflation_thms @ axs_deflation_take;
    1.14 -      val tacs =
    1.15 -          [simp_tac (HOL_basic_ss addsimps rules) 1,
    1.16 -           asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
    1.17 +      val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
    1.18      in pg con_appls goal (K tacs) end;
    1.19    val take_apps = map one_take_app cons;
    1.20  in