changeset 2979 | db6941221197 |
parent 2693 | 8300bba275e3 |
child 3767 | e2bb53d8dd26 |
--- a/src/Pure/theory.ML Thu Apr 17 18:45:43 1997 +0200 +++ b/src/Pure/theory.ML Thu Apr 17 18:46:58 1997 +0200 @@ -169,7 +169,7 @@ fun cert_axm sg (name, raw_tm) = let val (t, T, _) = Sign.certify_term sg raw_tm - handle TYPE arg => error (Sign.exn_type_msg sg arg) + handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; in assert (T = propT) "Term not of type prop";