# HG changeset patch
# User wenzelm
# Date 1380541517 -7200
# Node ID 4237859c186d90743607b6a89fb125adef9de4c0
# Parent  28fefe1d67492bc7cfde9685a662f1b78da0fac0
eliminated clone of Inductive.mk_cases_tac;

diff -r 28fefe1d6749 -r 4237859c186d src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:35:05 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:45:17 2013 +0200
@@ -17,19 +17,6 @@
 structure Fun_Cases : FUN_CASES =
 struct
 
-local
-
-val refl_thin =
-  Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
-    (fn _ => assume_tac 1);
-val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
-
-fun simp_case_tac ctxt i =
-  EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
-
-in
-
 fun mk_fun_cases ctxt prop =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -44,9 +31,9 @@
     val {elims, pelims, is_partial, ...} = info;
     val elims = if is_partial then pelims else the elims;
     val cprop = cterm_of thy prop;
-    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
     fun mk_elim rl =
-      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+      Thm.implies_intr cprop
+        (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
       |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in
     (case get_first (try mk_elim) (flat elims) of
@@ -54,9 +41,6 @@
     | NONE => err ())
   end;
 
-end;
-
-
 fun gen_fun_cases prep_att prep_prop args lthy =
   let
     val thy = Proof_Context.theory_of lthy;
diff -r 28fefe1d6749 -r 4237859c186d src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Sep 30 13:35:05 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Sep 30 13:45:17 2013 +0200
@@ -30,6 +30,7 @@
   val get_monos: Proof.context -> thm list
   val mono_add: attribute
   val mono_del: attribute
+  val mk_cases_tac: Proof.context -> tactic
   val mk_cases: Proof.context -> term -> thm
   val inductive_forall_def: thm
   val rulify: Proof.context -> thm -> thm
@@ -540,6 +541,8 @@
 
 in
 
+fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+
 fun mk_cases ctxt prop =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -551,9 +554,9 @@
     val elims = Induct.find_casesP ctxt prop;
 
     val cprop = Thm.cterm_of thy prop;
-    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
     fun mk_elim rl =
-      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+      Thm.implies_intr cprop
+        (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
       |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in
     (case get_first (try mk_elim) elims of