# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 9dfe8506c04ddfffb077fda303d96db016ebe63a
# Parent  c1c65a805d0f7110a27c52193791a5ee0fcdd5bd
tuned messages

diff -r c1c65a805d0f -r 9dfe8506c04d src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -58,7 +58,7 @@
 fun the_info thy name =
   (case get_info thy name of
     SOME info => info
-  | NONE => error ("Unknown datatype " ^ quote name));
+  | NONE => error ("Unknown old-style datatype " ^ quote name));
 
 fun info_of_constr thy (c, T) =
   let
@@ -169,7 +169,7 @@
       if eq_set (op =) (tycos, raw_tycos) then ()
       else
         error ("Type constructors " ^ commas_quote raw_tycos ^
-          " do not belong exhaustively to one mutual recursive datatype");
+          " do not belong exhaustively to one mutually recursive old-style datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;