# HG changeset patch
# User blanchet
# Date 1347483999 -7200
# Node ID d406979024d1b0f5dbc90c53d7d998bd3de3f5dd
# Parent  d1fcb4de8349a62002fe7f0296a6bc87391e0280
nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)

diff -r d1fcb4de8349 -r d406979024d1 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 22:00:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 23:06:39 2012 +0200
@@ -152,19 +152,21 @@
     (* nonemptiness check *)
     fun new_wit X wit = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
 
+    val all = m upto m + n - 1;
+
     fun enrich X = map_filter (fn i =>
       (case find_first (fn (_, i') => i = i') X of
         NONE =>
           (case find_index (new_wit X) (nth witss (i - m)) of
             ~1 => NONE
           | j => SOME (j, i))
-      | SOME ji => SOME ji)) (m upto m + n - 1);
+      | SOME ji => SOME ji)) all;
     val reachable = fixpoint (op =) enrich [];
-    val _ = if map snd reachable = (m upto m + n - 1) then ()
-      else error "The datatype could not be generated because nonemptiness could not be proved";
+    val _ = (case subtract (op =) (map snd reachable) all of
+        [] => ()
+      | i :: _ => error ("Invalid empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
 
-    val wit_thms =
-      flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
+    val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
 
     val timer = time (timer "Checked nonemptiness");