added betapplys;
authorwenzelm
Wed Nov 16 17:45:29 2005 +0100 (2005-11-16)
changeset 18183a9f67248996a
parent 18182 786d83044780
child 18184 43c4589a9a78
added betapplys;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Nov 16 17:45:28 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Nov 16 17:45:29 2005 +0100
     1.3 @@ -98,6 +98,7 @@
     1.4    val subst_bounds: term list * term -> term
     1.5    val subst_bound: term * term -> term
     1.6    val betapply: term * term -> term
     1.7 +  val betapplys: term * term list -> term
     1.8    val eq_ix: indexname * indexname -> bool
     1.9    val ins_ix: indexname * indexname list -> indexname list
    1.10    val mem_ix: indexname * indexname list -> bool
    1.11 @@ -804,6 +805,8 @@
    1.12  fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
    1.13    | betapply (f,u) = f$u;
    1.14  
    1.15 +val betapplys = Library.foldl betapply;
    1.16 +
    1.17  
    1.18  (** Specialized equality, membership, insertion etc. **)
    1.19