# HG changeset patch
# User wenzelm
# Date 978812853 -3600
# Node ID 2eba1c06592cab4853da4bc39b73ad1e0bc880a0
# Parent  89a29437cebcb334b78e3b27190d24d3a0681966
added list_abs;

diff -r 89a29437cebc -r 2eba1c06592c src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Jan 06 21:27:12 2001 +0100
+++ b/src/Pure/term.ML	Sat Jan 06 21:27:33 2001 +0100
@@ -51,6 +51,7 @@
   val type_of1: typ list * term -> typ
   val fastype_of: term -> typ
   val fastype_of1: typ list * term -> typ
+  val list_abs: (string * typ) list * term -> term
   val strip_abs_body: term -> term
   val strip_abs_vars: term -> (string * typ) list
   val strip_qnt_body: string -> term -> term
@@ -332,11 +333,12 @@
 fun fastype_of t : typ = fastype_of1 ([],t);
 
 
+val list_abs = foldr (fn ((x, T), t) => Abs (x, T, t));
+
 (* maps  (x1,...,xn)t   to   t  *)
 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t  
   | strip_abs_body u  =  u;
 
-
 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t 
   | strip_abs_vars u  =  [] : (string*typ) list;