# HG changeset patch
# User wenzelm
# Date 1002202783 -7200
# Node ID d9063229b4a198a7149259a792f17e1e96187afa
# Parent  f5a7b4b203be32b52d3d9d67fc438b10ca0f6f21
simp_case_tac is back again from induct_method.ML;
tuned;

diff -r f5a7b4b203be -r d9063229b4a1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:00 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:43 2001 +0200
@@ -295,7 +295,7 @@
 val all_not_allowed = 
     "Introduction rule must not have a leading \"!!\" quantifier";
 
-val atomize_cterm = hol_rewrite_cterm inductive_atomize;
+val atomize_cterm = full_rewrite_cterm inductive_atomize;
 
 in
 
@@ -543,14 +543,26 @@
   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   for inference systems. (??) *)
 
+local
+
 (*cprop should have the form t:Si where Si is an inductive set*)
+val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
 
-val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
+(*delete needless equality assumptions*)
+val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
+val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
+val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
+
+fun simp_case_tac solved ss i =
+  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
+  THEN_MAYBE (if solved then no_tac else all_tac);
+
+in
 
 fun mk_cases_i elims ss cprop =
   let
     val prem = Thm.assume cprop;
-    val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
+    val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   in
     (case get_first (try mk_elim) elims of
@@ -569,6 +581,8 @@
     val (_, {elims, ...}) = the_inductive thy c;
   in mk_cases_i elims ss cprop end;
 
+end;
+
 
 (* inductive_cases(_i) *)