src/HOL/Tools/Function/mutual.ML
changeset 53605 462151f900ea
parent 53603 59ef06cda7b9
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;