added dummy_pattern;

--- 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;