src/HOL/Tools/inductive.ML
changeset 53994 4237859c186d
parent 52732 b4da1f2ec73f
child 53995 1d457fc83f5c
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon Sep 30 13:35:05 2013 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Sep 30 13:45:17 2013 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val get_monos: Proof.context -> thm list
     1.5    val mono_add: attribute
     1.6    val mono_del: attribute
     1.7 +  val mk_cases_tac: Proof.context -> tactic
     1.8    val mk_cases: Proof.context -> term -> thm
     1.9    val inductive_forall_def: thm
    1.10    val rulify: Proof.context -> thm -> thm
    1.11 @@ -540,6 +541,8 @@
    1.12  
    1.13  in
    1.14  
    1.15 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.16 +
    1.17  fun mk_cases ctxt prop =
    1.18    let
    1.19      val thy = Proof_Context.theory_of ctxt;
    1.20 @@ -551,9 +554,9 @@
    1.21      val elims = Induct.find_casesP ctxt prop;
    1.22  
    1.23      val cprop = Thm.cterm_of thy prop;
    1.24 -    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.25      fun mk_elim rl =
    1.26 -      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    1.27 +      Thm.implies_intr cprop
    1.28 +        (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
    1.29        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    1.30    in
    1.31      (case get_first (try mk_elim) elims of