added dummy_pattern;
authorwenzelm
Fri Nov 25 18:58:40 2005 +0100 (2005-11-25)
changeset 182530626a0a217ec
parent 18252 9e2c15ae0e86
child 18254 4a081083b06e
added dummy_pattern;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Nov 25 18:58:38 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Nov 25 18:58:40 2005 +0100
     1.3 @@ -202,6 +202,7 @@
     1.4    val zero_var_indexes_inst: term ->
     1.5      ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     1.6    val dummy_patternN: string
     1.7 +  val dummy_pattern: typ -> term
     1.8    val no_dummy_patterns: term -> term
     1.9    val replace_dummy_patterns: int * term -> int * term
    1.10    val is_replaced_dummy_pattern: indexname -> bool
    1.11 @@ -1282,6 +1283,8 @@
    1.12  
    1.13  val dummy_patternN = "dummy_pattern";
    1.14  
    1.15 +fun dummy_pattern T = Const (dummy_patternN, T);
    1.16 +
    1.17  fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
    1.18    | is_dummy_pattern _ = false;
    1.19