Improved error handling: if there are syntax or type-checking
errors, prints the name of the offending axiom

--- a/src/Pure/theory.ML	Fri Sep 06 10:45:48 1996 +0200
+++ b/src/Pure/theory.ML	Fri Sep 06 11:56:12 1996 +0200
@@ -171,7 +171,8 @@
   let val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
       val (_, t, _) =
           Sign.infer_types sg (K None) (K None) [] true (ts,propT);
-  in cert_axm sg (name,t) end;
+  in cert_axm sg (name,t) end
+  handle ERROR => err_in_axm name;
 
 fun inferT_axm sg (name, pre_tm) =
   let val t = #2(Sign.infer_types sg (K None) (K None) [] true