--- 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. **)