tuned error handling;

--- a/src/Pure/theory.ML	Thu Aug 17 10:39:12 2000 +0200
+++ b/src/Pure/theory.ML	Thu Aug 17 10:39:30 2000 +0200
@@ -249,8 +249,7 @@
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     assert (T = propT) "Term not of type prop";
     (name, no_vars t)
-  end
-  handle ERROR => err_in_axm name;
+  end;
 
 (*some duplication of code with read_def_cterm*)
 fun read_def_axm (sg, types, sorts) used (name, str) =