--- a/src/Pure/Syntax/syn_trans.ML Mon Feb 06 20:59:57 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Mon Feb 06 20:59:58 2006 +0100
@@ -20,6 +20,7 @@
val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
val mark_bound: string -> term
val mark_boundT: string * typ -> term
+ val bound_vars: (string * typ) list -> term -> term
val variant_abs': string * typ * term -> string * term
val fixedN: string
end;
@@ -237,6 +238,9 @@
fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T;
fun mark_bound x = mark_boundT (x, dummyT);
+fun bound_vars vars body =
+ subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
+
fun strip_abss vars_of body_of tm =
let
val vars = vars_of tm;