--- a/src/HOL/Tools/datatype_package.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Apr 14 15:58:01 1999 +0200
@@ -529,7 +529,7 @@
val sorts = add_term_tfrees (concl_of induction', []);
val dt_info = get_datatypes thy1;
- val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
+ val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val (thy2, casedist_thms) = thy1 |>
DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;