dropped dead code
authorkrauss
Sun, 08 Sep 2013 23:28:27 +0200
changeset 53605 462151f900ea
parent 53604 c1db98d7c66f
child 53606 c3f7070dd05a
dropped dead code
src/HOL/Tools/Function/mutual.ML
--- 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;