# HG changeset patch
# User wenzelm
# Date 963481331 -7200
# Node ID 7d9b562a750b25e941b25576323c518ef66ec868
# Parent  bafe45732b106b4396ef50bd4ba0e1b2d1d9dcf6
use InductMethod.simp_case_tac;

diff -r bafe45732b10 -r 7d9b562a750b src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:41:40 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:42:11 2000 +0200
@@ -476,8 +476,8 @@
 fun mk_cases_i solved elims ss cprop =
   let
     val prem = Thm.assume cprop;
-    val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
-    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
+    val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
+    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   in
     (case get_first (try mk_elim) elims of
       Some r => r