# HG changeset patch
# User wenzelm
# Date 1139255998 -3600
# Node ID 9151a29d2864e89b714f77f1bfb3480315e0565c
# Parent  8c3abd63bce3ac2e9e3d6240a500aab588638a1c
added bound_vars;

diff -r 8c3abd63bce3 -r 9151a29d2864 src/Pure/Syntax/syn_trans.ML
--- 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;