# HG changeset patch
# User desharna
# Date 1408622385 -7200
# Node ID 95d6488f12043e5ab76f025d70acc1174eaf0212
# Parent  8179d1369567309685ddcbffba7fc7db7eeb5749
fix tactic failure with rel_induct0

minimal example:

datatype_new 'a A1 = A1 nat
         and 'a A2 = A2 'a

diff -r 8179d1369567 -r 95d6488f1204 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Aug 20 20:50:28 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Aug 21 13:59:45 2014 +0200
@@ -283,7 +283,7 @@
         TRYALL (hyp_subst_tac ctxt) THEN
         unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
           Inr_Inl_False  sum.inject prod.inject}) THEN
-        TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
+        TRYALL (rtac refl ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
     cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
 
 fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts =