use InductMethod.simp_case_tac;
authorwenzelm
Thu Jul 13 11:42:11 2000 +0200 (2000-07-13)
changeset 92987d9b562a750b
parent 9297 bafe45732b10
child 9299 c5cda71de65d
use InductMethod.simp_case_tac;
src/HOL/Tools/inductive_package.ML
     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