added lambda;
authorwenzelm
Wed Oct 24 17:38:19 2001 +0200 (2001-10-24)
changeset 1192278857e6107cb
parent 11921 2a0e9622dc51
child 11923 929d97ed8c0f
added lambda;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Oct 24 17:37:58 2001 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Oct 24 17:38:19 2001 +0200
     1.3 @@ -126,6 +126,7 @@
     1.4    val atless: term * term -> bool
     1.5    val insert_aterm: term * term list -> term list
     1.6    val abstract_over: term * term -> term
     1.7 +  val lambda: term -> term -> term
     1.8    val absfree: string * typ * term -> term
     1.9    val list_abs_free: (string * typ) list * term -> term
    1.10    val list_all_free: (string * typ) list * term -> term
    1.11 @@ -617,6 +618,9 @@
    1.12          | _ => u)
    1.13    in  abst(0,body)  end;
    1.14  
    1.15 +fun lambda v t =
    1.16 +  let val (x, T) = dest_Free v
    1.17 +  in Abs (x, T, abstract_over (v, t)) end;
    1.18  
    1.19  (*Form an abstraction over a free variable.*)
    1.20  fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));