--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 20:10:08 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 20:25:40 2014 +0100
@@ -77,14 +77,12 @@
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
- disc_same_tac
+ REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
else
dtac fun_disc' THEN' (REPEAT_DETERM o atac) THEN'
DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac))