# HG changeset patch
# User wenzelm
# Date 965422801 -7200
# Node ID 7e0ba737f98e8acd147a19b2ab852fffd98827ba
# Parent  b79b002f32aeff65479f97444a077260bb121f02
axioms: Term.no_dummy_patterns;

diff -r b79b002f32ae -r 7e0ba737f98e src/Pure/theory.ML
--- 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