src/HOL/Tools/Old_Datatype/old_datatype_data.ML

 val get_info = Symtab.lookup o get_all;
 
 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
     val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
   in

     val tycos = map fst dataTs;
     val _ =
       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;
 
     val names = map Long_Name.base_name tycos;
     val (auxnames, _) =