tuned error message
authorblanchet
Sat Sep 15 21:10:26 2012 +0200 (2012-09-15)
changeset 49390a4202c1f4f9d
parent 49389 da621dc65146
child 49391 3a96797fd53e
tuned error message
src/HOL/Codatatype/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 15 21:10:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4      val reachable = fixpoint (op =) enrich [];
     1.5      val _ = (case subtract (op =) (map snd reachable) all of
     1.6          [] => ()
     1.7 -      | i :: _ => error ("Invalid empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
     1.8 +      | i :: _ => error ("Cannot define empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
     1.9  
    1.10      val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
    1.11