made tactic more robust w.r.t. equations containing 'case_prod'
authorblanchet
Thu, 16 Jul 2015 17:25:44 +0200
changeset 60729 cf291b55f3d1
parent 60728 26ffdb966759
child 60730 c4bc0691860b
made tactic more robust w.r.t. equations containing 'case_prod'
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