# HG changeset patch
# User blanchet
# Date 1380201208 -7200
# Node ID c6de7f20c845af8df766a47f41a63070f3e01625
# Parent  6f9dbc063ae6cdd5205d120bdb999595042ca68a
made tactic more robust in case somebody specified a discriminator for a one-constructor type

diff -r 6f9dbc063ae6 -r c6de7f20c845 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Thu Sep 26 13:56:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Thu Sep 26 15:13:28 2013 +0200
@@ -65,8 +65,8 @@
 val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
 
 fun mk_sel_exhaust_tac n disc_exhaust collapses =
-  if n = 1 then HEADGOAL (etac meta_mp THEN' resolve_tac collapses)
-  else mk_disc_or_sel_exhaust_tac n disc_exhaust collapses;
+  mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
+  HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
 
 fun mk_collapse_tac ctxt m discD sels =
   HEADGOAL (dtac discD THEN'