--- 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;