# HG changeset patch
# User traytel
# Date 1378977829 -7200
# Node ID 9d8764624487d83cd2397182d35d449d8cf4647c
# Parent  92bcac4f9ac9b054b9146f86b7173a643de9e71b
handle corner case in tactic

diff -r 92bcac4f9ac9 -r 9d8764624487 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
@@ -222,16 +222,18 @@
   {context = ctxt, prems = _} =
   let
     val n = length set_maps;
+    val in_tac = if n = 0 then rtac UNIV_I else
+      rtac CollectI THEN' CONJ_WRAP' (fn thm =>
+        etac (thm RS
+          @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
+      set_maps;
   in
     REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
     unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
       rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
       REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
-      rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-      CONJ_WRAP' (fn thm =>
-        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
-      set_maps,
+      rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac,
       rtac conjI,
       EVERY' (map (fn convol =>
         rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'