# HG changeset patch
# User blanchet
# Date 1388692269 -3600
# Node ID a426e38a8a7eb86be0364ff6f1126e49816d6623
# Parent  aa891e065af128c239de6e192768ff0758bc8e39
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly

diff -r aa891e065af1 -r a426e38a8a7e src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 20:25:40 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 20:51:09 2014 +0100
@@ -1208,7 +1208,7 @@
                 []
               else
                 mk_primcorec_disc_iff_tac lthy (the_single exhaust_thms) (the_single disc_thms)
-                  (flat disc_thmss) (flat disc_excludess)
+                  disc_thmss (flat disc_excludess)
                 |> K |> Goal.prove lthy [] [] goal
                 |> Thm.close_derivation
                 |> single
diff -r aa891e065af1 -r a426e38a8a7e src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 20:25:40 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 20:51:09 2014 +0100
@@ -12,7 +12,7 @@
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
-  val mk_primcorec_disc_iff_tac: Proof.context -> thm -> thm -> thm list -> thm list -> tactic
+  val mk_primcorec_disc_iff_tac: Proof.context -> thm -> thm -> thm list list -> thm list -> tactic
   val mk_primcorec_exhaust_tac: int -> thm -> tactic
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> thm option -> tactic
@@ -77,16 +77,17 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discs disc_excludes =
+fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discss disc_excludes =
   HEADGOAL (rtac iffI THEN'
     rtac fun_exhaust THEN'
-    EVERY' (map (fn fun_disc' =>
-        if Thm.eq_thm (fun_disc', fun_disc) then
-          REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
-        else
-          dtac fun_disc' THEN' (REPEAT_DETERM o atac) THEN'
-          DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac))
-      fun_discs) THEN'
+    EVERY' (map (fn [] => etac FalseE
+        | [fun_disc'] =>
+          if Thm.eq_thm (fun_disc', fun_disc) then
+            REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
+          else
+            rtac FalseE THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
+            DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac))
+      fun_discss) THEN'
     rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m