# HG changeset patch
# User wenzelm
# Date 1132941520 -3600
# Node ID 0626a0a217ec8fe4bccb046384a560c8da72d848
# Parent  9e2c15ae0e86989e551b2d51891243a8d8db4533
added dummy_pattern;

diff -r 9e2c15ae0e86 -r 0626a0a217ec src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Nov 25 18:58:38 2005 +0100
+++ b/src/Pure/term.ML	Fri Nov 25 18:58:40 2005 +0100
@@ -202,6 +202,7 @@
   val zero_var_indexes_inst: term ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   val dummy_patternN: string
+  val dummy_pattern: typ -> term
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: int * term -> int * term
   val is_replaced_dummy_pattern: indexname -> bool
@@ -1282,6 +1283,8 @@
 
 val dummy_patternN = "dummy_pattern";
 
+fun dummy_pattern T = Const (dummy_patternN, T);
+
 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
   | is_dummy_pattern _ = false;