# HG changeset patch
# User haftmann
# Date 1168327906 -3600
# Node ID 70583c3f3fa537c702b8ef6aea313f5dae5db326
# Parent  91f1731b57c2ec8410c6fd68f27b05ceadc0ccb4
added map_abs_vars

diff -r 91f1731b57c2 -r 70583c3f3fa5 src/Pure/term.ML
--- 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, []);