src/HOL/Tools/inductive_package.ML
changeset 9298 7d9b562a750b
parent 9235 1f734dc2e526
child 9315 f793f05024f6
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:41:40 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:42:11 2000 +0200
     1.3 @@ -476,8 +476,8 @@
     1.4  fun mk_cases_i solved elims ss cprop =
     1.5    let
     1.6      val prem = Thm.assume cprop;
     1.7 -    val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
     1.8 -    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
     1.9 +    val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
    1.10 +    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
    1.11    in
    1.12      (case get_first (try mk_elim) elims of
    1.13        Some r => r