src/Pure/theory.ML

   else error "Illegal schematic variable(s) in term";
 
 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";
     (name, no_vars t)
   end