Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made tactic more robust in case somebody specified a discriminator for a one-constructor type
authorblanchet
Thu, 26 Sep 2013 15:13:28 +0200
changeset 53920 c6de7f20c845
parent 53919 6f9dbc063ae6
child 53921 46fc95abef09
made tactic more robust in case somebody specified a discriminator for a one-constructor type
src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- 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'
isabelle