--- a/src/Pure/term.ML Mon Jan 08 12:26:13 2007 +0100
+++ b/src/Pure/term.ML Tue Jan 09 08:31:46 2007 +0100
@@ -173,6 +173,7 @@
val termless: term * term -> bool
val term_lpo: (term -> int) -> term * term -> order
val match_bvars: (term * term) * (string * string) list -> (string * string) list
+ val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
val eq_var: (indexname * typ) * (indexname * typ) -> bool
@@ -761,6 +762,10 @@
(* strip abstractions created by parameters *)
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
+fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
+ | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
+ | map_abs_vars f t = t;
+
fun rename_abs pat obj t =
let
val ren = match_bvs (pat, obj, []);