# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 63db983c695319fa387a1902c3e5ea9d0dd9466d
# Parent  f4ae538b0ba5ea9accd23abeb8f834e61d4f405c
graceful handling of one-constructor case

diff -r f4ae538b0ba5 -r 63db983c6953 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -968,6 +968,8 @@
 
     fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
 
+    val p_imp_p = mk_imp_p [mk_imp_p []];
+
     fun prove thmss'' def_thms' lthy =
       let
         val def_thms = map (snd o snd) def_thms';
@@ -987,6 +989,8 @@
                  |> K |> Goal.prove lthy [] [] goal
                  |> Thm.close_derivation])
             disc_eqnss nchotomy_thmss;
+        val nontriv_exhaust_thmss =
+          map (filter_out (fn thm => prop_of thm aconv p_imp_p)) exhaust_thmss;
 
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
         fun mk_excludesss excludes n =
@@ -1224,7 +1228,7 @@
            (discN, disc_thmss, simp_attrs),
            (disc_iffN, disc_iff_thmss, []),
            (excludeN, exclude_thmss, []),
-           (exhaustN, exhaust_thmss, []),
+           (exhaustN, nontriv_exhaust_thmss, []),
            (selN, sel_thmss, simp_attrs),
            (simpsN, simp_thmss, []),
            (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
diff -r f4ae538b0ba5 -r 63db983c6953 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -86,12 +86,12 @@
       rtac fun_exhaust THEN'
       EVERY' (map2 (fn k' => fn disc =>
           if k' = k then
-            REPEAT_DETERM o (atac ORELSE' etac conjI)
+            REPEAT_DETERM o (atac ORELSE' rtac TrueI ORELSE' etac conjI)
           else
             dtac disc THEN' (REPEAT_DETERM o atac) THEN' dresolve_tac disc_excludes THEN'
             etac notE THEN' atac)
         ks fun_discs) THEN'
-      etac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))))
+      rtac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))) THEN_MAYBE' atac)
   end;
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m