# HG changeset patch
# User wenzelm
# Date 966501570 -7200
# Node ID 50f1c4222aeacb06b84935ae9e82d548aacbd00e
# Parent  53a62fd8b2dcaec20b757712bcc1111efa69f473
tuned error handling;

diff -r 53a62fd8b2dc -r 50f1c4222aea src/Pure/theory.ML
--- 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) =