made tactic more robust w.r.t. equations containing 'case_prod'
authorblanchet
Thu Jul 16 17:25:44 2015 +0200 (2015-07-16)
changeset 60735cf291b55f3d1
parent 60728 26ffdb966759
child 60736 c4bc0691860b
made tactic more robust w.r.t. equations containing 'case_prod'
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 12:23:22 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 17:25:44 2015 +0200
     1.3 @@ -82,9 +82,11 @@
     1.4      etac ctxt notE THEN' atac ORELSE'
     1.5      etac ctxt disjE))));
     1.6  
     1.7 -fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
     1.8 +fun ss_fst_snd_conv ctxt =
     1.9 +  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
    1.10  
    1.11 -fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
    1.12 +fun case_atac ctxt =
    1.13 +  Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
    1.14  
    1.15  fun same_case_tac ctxt m =
    1.16    HEADGOAL (if m = 0 then rtac ctxt TrueI