# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID f57c4bb105757dbc34006bc2c758276e06e998ca
# Parent  3c5eba97d93adee8aeb27d5d5544f43c5fb6ca4a
optimized "case_cong" proof

diff -r 3c5eba97d93a -r f57c4bb10575 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -28,7 +28,7 @@
   thm RS @{thm eq_False[THEN iffD2]}
   handle THM _ => thm RS @{thm eq_True[THEN iffD2]}
 
-fun ss_only thms ss = Simplifier.clear_ss ss addsimps thms
+fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
 
 fun mk_nchotomy_tac n exhaust =
   (rtac allI THEN' rtac exhaust THEN'
@@ -68,14 +68,15 @@
   end;
 
 fun mk_case_cong_tac ctxt exhaust' case_thms =
-  rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (map_simpset (ss_only case_thms) ctxt));
+  (rtac exhaust' THEN'
+   EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
 
 val naked_ctxt = Proof_Context.init_global @{theory HOL};
 
 fun mk_split_tac ctxt exhaust' case_thms injects distincts =
   rtac exhaust' 1 THEN
   ALLGOALS (hyp_subst_tac THEN'
-    simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
+    simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts))) THEN
   ALLGOALS (blast_tac naked_ctxt);
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};