--- 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;