| changeset 4974 | 45b7a51342a1 |
| parent 4970 | 8b65444edbb0 |
| child 4996 | 951575080635 |
--- 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)) =