# 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, []);