# HG changeset patch
# User wenzelm
# Date 1176836819 -7200
# Node ID a3a856313bcf2cd892282634e92f09b7cbda26c0
# Parent  704de05715b4a3018b8dd1125aae5399e23229bb
export is_dummy_pattern;

diff -r 704de05715b4 -r a3a856313bcf src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Apr 17 03:13:38 2007 +0200
+++ b/src/Pure/term.ML	Tue Apr 17 21:06:59 2007 +0200
@@ -187,6 +187,7 @@
   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   val dummy_patternN: string
   val dummy_pattern: typ -> term
+  val is_dummy_pattern: term -> bool
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: int * term -> int * term
   val is_replaced_dummy_pattern: indexname -> bool