# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 7b18c41df27ab9b5438635129ea2396fcd63045f
# Parent  4ecdea61181e39cc4454bfaf2f7748d09208f35d
consider code as exhaustive

diff -r 4ecdea61181e -r 7b18c41df27a 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
@@ -939,7 +939,8 @@
         disc_eqnss;
 
     val syntactic_exhaustives =
-      map (fn disc_eqns => forall (null o #prems) disc_eqns orelse exists #auto_gen disc_eqns)
+      map (fn disc_eqns => forall (null o #prems orf is_some o #maybe_code_rhs) disc_eqns
+          orelse exists #auto_gen disc_eqns)
         disc_eqnss;
     val de_facto_exhaustives =
       map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;