fix 'set_empty' theorem when the discriminator is 'op ='
authordesharna
Mon May 19 09:35:35 2014 +0200 (2014-05-19)
changeset 56990299b026cc5af
parent 56989 fafcf43ded4a
child 56991 8e9ca31e9b8e
fix 'set_empty' theorem when the discriminator is 'op ='
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun May 18 20:29:04 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon May 19 09:35:35 2014 +0200
     1.3 @@ -195,8 +195,8 @@
     1.4  fun mk_set_empty_tac ctxt ct exhaust sets discs =
     1.5    TRYALL Goal.conjunction_tac THEN
     1.6    ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
     1.7 -    hyp_subst_tac ctxt) THEN
     1.8 -  Local_Defs.unfold_tac ctxt (sets @ map_filter (fn thm =>
     1.9 +    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.10 +  unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
    1.11      SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
    1.12    ALLGOALS(rtac refl ORELSE' etac FalseE);
    1.13