src/HOL/Tools/inductive_package.ML
changeset 9298 7d9b562a750b
parent 9235 1f734dc2e526
child 9315 f793f05024f6
equal deleted inserted replaced
9297:bafe45732b10 9298:7d9b562a750b
   474 
   474 
   475 (*cprop should have the form t:Si where Si is an inductive set*)
   475 (*cprop should have the form t:Si where Si is an inductive set*)
   476 fun mk_cases_i solved elims ss cprop =
   476 fun mk_cases_i solved elims ss cprop =
   477   let
   477   let
   478     val prem = Thm.assume cprop;
   478     val prem = Thm.assume cprop;
   479     val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
   479     val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
   480     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
   480     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   481   in
   481   in
   482     (case get_first (try mk_elim) elims of
   482     (case get_first (try mk_elim) elims of
   483       Some r => r
   483       Some r => r
   484     | None => error (Pretty.string_of (Pretty.block
   484     | None => error (Pretty.string_of (Pretty.block
   485         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
   485         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,