diff -r 83a4c4f79dcd -r db6941221197 src/Pure/theory.ML
--- 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";