# HG changeset patch
# User blanchet
# Date 1389363743 -3600
# Node ID b502f04c0442322f875353f0ae418d37d8a53bfe
# Parent  451786451d040e4e851af4d43808f4251f0c866a
repair 'exhaustive' feature for one-constructor types

diff -r 451786451d04 -r b502f04c0442 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 15:11:00 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 15:22:23 2014 +0100
@@ -632,9 +632,11 @@
       handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
 
     val disc_concl = betapply (disc, lhs);
-    val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1
-      then (NONE, matchedsss)
-      else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
+    val (eqn_data_disc_opt, matchedsss') =
+      if null (tl basic_ctr_specs) then
+        (NONE, matchedsss)
+      else
+        apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
           (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
 
     val sel_concls = sels ~~ ctr_args
@@ -1243,7 +1245,7 @@
         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
             (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
-          if null exhaust_thms then
+          if null exhaust_thms orelse null (tl ctr_specs) then
             []
           else
             let