# HG changeset patch
# User blanchet
# Date 1347736226 -7200
# Node ID a4202c1f4f9d46927eedd2496ddd7c5fce4ad18a
# Parent  da621dc65146775748f07bd0fc116a25d55492f3
tuned error message

diff -r da621dc65146 -r a4202c1f4f9d src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 15 21:10:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -164,7 +164,7 @@
     val reachable = fixpoint (op =) enrich [];
     val _ = (case subtract (op =) (map snd reachable) all of
         [] => ()
-      | i :: _ => error ("Invalid empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
+      | i :: _ => error ("Cannot define 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);