# HG changeset patch
# User wenzelm
# Date 1132159529 -3600
# Node ID a9f67248996a737ce92d49c002972c2929b95d5c
# Parent  786d8304478008d3f6164b6e6a9c4e781f41dc2a
added betapplys;

diff -r 786d83044780 -r a9f67248996a src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Nov 16 17:45:28 2005 +0100
+++ b/src/Pure/term.ML	Wed Nov 16 17:45:29 2005 +0100
@@ -98,6 +98,7 @@
   val subst_bounds: term list * term -> term
   val subst_bound: term * term -> term
   val betapply: term * term -> term
+  val betapplys: term * term list -> term
   val eq_ix: indexname * indexname -> bool
   val ins_ix: indexname * indexname list -> indexname list
   val mem_ix: indexname * indexname list -> bool
@@ -804,6 +805,8 @@
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   | betapply (f,u) = f$u;
 
+val betapplys = Library.foldl betapply;
+
 
 (** Specialized equality, membership, insertion etc. **)