src/HOL/Tools/inductive_package.ML
changeset 9298 7d9b562a750b
parent 9235 1f734dc2e526
child 9315 f793f05024f6
--- 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