axioms: Term.no_dummy_patterns;

--- a/src/Pure/theory.ML	Fri Aug 04 22:59:33 2000 +0200
+++ b/src/Pure/theory.ML	Fri Aug 04 23:00:01 2000 +0200
@@ -246,6 +246,7 @@
       handle TYPE (msg, _, _) => error msg
            | TERM (msg, _) => error msg;
   in
+    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     assert (T = propT) "Term not of type prop";
     (name, no_vars t)
   end