# HG changeset patch
# User wenzelm
# Date 1003937899 -7200
# Node ID 78857e6107cb813aaa06445d7cfababfc17630c5
# Parent  2a0e9622dc513142ccd1946306bbb4fd8c747ae4
added lambda;

diff -r 2a0e9622dc51 -r 78857e6107cb src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Oct 24 17:37:58 2001 +0200
+++ b/src/Pure/term.ML	Wed Oct 24 17:38:19 2001 +0200
@@ -126,6 +126,7 @@
   val atless: term * term -> bool
   val insert_aterm: term * term list -> term list
   val abstract_over: term * term -> term
+  val lambda: term -> term -> term
   val absfree: string * typ * term -> term
   val list_abs_free: (string * typ) list * term -> term
   val list_all_free: (string * typ) list * term -> term
@@ -617,6 +618,9 @@
         | _ => u)
   in  abst(0,body)  end;
 
+fun lambda v t =
+  let val (x, T) = dest_Free v
+  in Abs (x, T, abstract_over (v, t)) end;
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));