author | krauss |
Sun, 08 Sep 2013 23:28:27 +0200 | |
changeset 53605 | 462151f900ea |
parent 53604 | c1db98d7c66f |
child 53606 | c3f7070dd05a |
--- a/src/HOL/Tools/Function/mutual.ML Sun Sep 08 23:26:08 2013 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Sun Sep 08 23:28:27 2013 +0200 @@ -321,8 +321,6 @@ fun prep_subgoal i = REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format] Inr_inject[elim_format]} i) -(* THEN propagate_tac i*) -(* THEN bool_subst_tac ctxt i*) THEN REPEAT (Tactic.eresolve_tac sum_elims i); val tac = ALLGOALS prep_subgoal;