src/Pure/term.ML
changeset 22031 70583c3f3fa5
parent 21975 1152dc45d591
child 22572 c6bbe56afbf7
     1.1 --- a/src/Pure/term.ML	Mon Jan 08 12:26:13 2007 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Jan 09 08:31:46 2007 +0100
     1.3 @@ -173,6 +173,7 @@
     1.4    val termless: term * term -> bool
     1.5    val term_lpo: (term -> int) -> term * term -> order
     1.6    val match_bvars: (term * term) * (string * string) list -> (string * string) list
     1.7 +  val map_abs_vars: (string -> string) -> term -> term
     1.8    val rename_abs: term -> term -> term -> term option
     1.9    val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
    1.10    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.11 @@ -761,6 +762,10 @@
    1.12  (* strip abstractions created by parameters *)
    1.13  fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
    1.14  
    1.15 +fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
    1.16 +  | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
    1.17 +  | map_abs_vars f t = t;
    1.18 +
    1.19  fun rename_abs pat obj t =
    1.20    let
    1.21      val ren = match_bvs (pat, obj, []);