# HG changeset patch
# User krauss
# Date 1378675707 -7200
# Node ID 462151f900ea935ac5e94a4873a6f9432b839547
# Parent  c1db98d7c66f8956141230345d85913f70a06818
dropped dead code

diff -r c1db98d7c66f -r 462151f900ea 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;