# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 4ecdea61181e39cc4454bfaf2f7748d09208f35d
# Parent  6a6980245ce07892460ce697113156d81b90c14b
proper handling of corner case, take 2

diff -r 6a6980245ce0 -r 4ecdea61181e 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
@@ -811,7 +811,7 @@
 fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec)
     (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =
   let val num_disc_eqns = length disc_eqns in
-    if num_disc_eqns < length ctr_specs - 1 andalso num_disc_eqns > 1 then
+    if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs - 1 then
       disc_eqns
     else
       let