# HG changeset patch
# User blanchet
# Date 1437060344 -7200
# Node ID cf291b55f3d163a86d294245f12f9a23ef0a83e1
# Parent  26ffdb9667598195681e346db8ce3370c656cc01
made tactic more robust w.r.t. equations containing 'case_prod'

diff -r 26ffdb966759 -r cf291b55f3d1 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 12:23:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 17:25:44 2015 +0200
@@ -82,9 +82,11 @@
     etac ctxt notE THEN' atac ORELSE'
     etac ctxt disjE))));
 
-fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
+fun ss_fst_snd_conv ctxt =
+  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
 
-fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
+fun case_atac ctxt =
+  Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
 
 fun same_case_tac ctxt m =
   HEADGOAL (if m = 0 then rtac ctxt TrueI