# HG changeset patch
# User blanchet
# Date 1457389211 -3600
# Node ID cb262f03ac122f50eddb0334f563ffc560917472
# Parent  6855b348e828081db1614200ea3f9c418cc904f6
strengthened tactic

diff -r 6855b348e828 -r cb262f03ac12 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 07 15:57:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 07 23:20:11 2016 +0100
@@ -117,8 +117,8 @@
 fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
   HEADGOAL Goal.conjunction_tac THEN
   ALLGOALS (REPEAT o (resolve_tac ctxt (rel_funI :: rel_intros) THEN'
-    TRY o (REPEAT_DETERM1 o (assume_tac ctxt ORELSE'
-      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac ctxt refl))));
+    TRY o (REPEAT_DETERM1 o (SELECT_GOAL (unfold_thms_tac ctxt rel_eqs) THEN'
+      (assume_tac ctxt ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt refl)))));
 
 fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc =
   let