# HG changeset patch
# User paulson
# Date 842003772 -7200
# Node ID ae390b599213f34362f6248a5d9aa81f7925bf29
# Parent  58f8379eca731c6e604e47fd68c13994285b8745
Improved error handling: if there are syntax or type-checking
errors, prints the name of the offending axiom

diff -r 58f8379eca73 -r ae390b599213 src/Pure/theory.ML
--- 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