1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.3 @@ -939,7 +939,8 @@
     1.4          disc_eqnss;
     1.5  
     1.6      val syntactic_exhaustives =
     1.7 -      map (fn disc_eqns => forall (null o #prems) disc_eqns orelse exists #auto_gen disc_eqns)
     1.8 +      map (fn disc_eqns => forall (null o #prems orf is_some o #maybe_code_rhs) disc_eqns
     1.9 +          orelse exists #auto_gen disc_eqns)
    1.10          disc_eqnss;
    1.11      val de_facto_exhaustives =
    1.12        map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;