# HG changeset patch
# User blanchet
# Date 1388690740 -3600
# Node ID aa891e065af128c239de6e192768ff0758bc8e39
# Parent  61284fe0536a48ecc8648b00b266c24425efccb0
simplified code

diff -r 61284fe0536a -r aa891e065af1 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- 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))