# HG changeset patch # User blanchet # Date 1388689808 -3600 # Node ID 61284fe0536a48ecc8648b00b266c24425efccb0 # Parent 25212efcd0de9a5816cf75df0f5dfdeb89ceea66 prevent tactic from getting out of sync and wrongly attack next subgoal diff -r 25212efcd0de -r 61284fe0536a src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 19:07:36 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 20:10:08 2014 +0100 @@ -77,15 +77,17 @@ fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss; +fun disc_same_tac i st = (atac ORELSE' rtac TrueI ORELSE' etac conjI THEN' disc_same_tac) i st; + fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discs disc_excludes = HEADGOAL (rtac iffI THEN' rtac fun_exhaust THEN' EVERY' (map (fn fun_disc' => if Thm.eq_thm (fun_disc', fun_disc) then - REPEAT_DETERM o (atac ORELSE' rtac TrueI ORELSE' etac conjI) + disc_same_tac else - dtac fun_disc' THEN' (REPEAT_DETERM o atac) THEN' dresolve_tac disc_excludes THEN' - etac notE THEN' atac) + dtac fun_disc' THEN' (REPEAT_DETERM o atac) THEN' + DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac)) fun_discs) THEN' rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);