# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1457965511 0
# Node ID 7f17ebd3293ec3a08f38502ec79e111172073313
# Parent  f7f2467ab85451b435a7c937a2ff6f5d7e280b43# Parent  b5ec623952d2ddfc59e4e5a42b2d60ae3ddfa935
Merge

diff -r f7f2467ab854 -r 7f17ebd3293e src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Mar 14 14:19:06 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Mar 14 14:25:11 2016 +0000
@@ -106,7 +106,7 @@
   in
     if null set_maps then
       unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
-      rtac ctxt @{thm Grp_UNIV_idI[OF refl]} 1
+      resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1
     else
       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
         REPEAT_DETERM o eresolve_tac ctxt
@@ -139,7 +139,7 @@
 fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 =
   (EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN'
   rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
-  (if n = 0 then rtac ctxt refl
+  (if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl
   else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
     rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, rtac ctxt subsetI, rtac ctxt CollectI,
     CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;