src/Pure/term.ML
changeset 17786 f06d6498ebf0
parent 17777 05f5532a8289
child 17851 2fa4f9b54761
     1.1 --- a/src/Pure/term.ML	Fri Oct 07 22:59:23 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Oct 07 22:59:24 2005 +0200
     1.3 @@ -112,6 +112,7 @@
     1.4    val abstract_over: term * term -> term
     1.5    val lambda: term -> term -> term
     1.6    val absfree: string * typ * term -> term
     1.7 +  val absdummy: typ * term -> term
     1.8    val list_abs_free: (string * typ) list * term -> term
     1.9    val list_all_free: (string * typ) list * term -> term
    1.10    val list_all: (string * typ) list * term -> term
    1.11 @@ -894,6 +895,7 @@
    1.12  
    1.13  (*Form an abstraction over a free variable.*)
    1.14  fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
    1.15 +fun absdummy (T, body) = Abs ("uu", T, body);
    1.16  
    1.17  (*Abstraction over a list of free variables*)
    1.18  fun list_abs_free ([ ] ,     t) = t