--- a/src/Pure/theory.ML Wed May 27 12:25:56 1998 +0200
+++ b/src/Pure/theory.ML Thu May 28 11:08:45 1998 +0200
@@ -355,7 +355,7 @@
(* check_defn *)
fun err_in_defn sg name msg =
- (writeln msg; error ("The error(s) above occurred in definition " ^
+ (error_msg msg; error ("The error(s) above occurred in definition " ^
quote (Sign.full_name sg name)));
fun check_defn sign (axms, (name, tm)) =
--- a/src/Pure/type.ML Wed May 27 12:25:56 1998 +0200
+++ b/src/Pure/type.ML Thu May 28 11:08:45 1998 +0200
@@ -573,7 +573,7 @@
fun prep_abbr tsig (a, vs, raw_rhs) =
let
- fun err msgs = (seq writeln msgs;
+ fun err msgs = (seq error_msg msgs;
error ("The error(s) above occurred in type abbreviation " ^ quote a));
val rhs = rem_sorts (varifyT (no_tvars raw_rhs))