1.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Feb 06 20:59:57 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon Feb 06 20:59:58 2006 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
     1.5    val mark_bound: string -> term
     1.6    val mark_boundT: string * typ -> term
     1.7 +  val bound_vars: (string * typ) list -> term -> term
     1.8    val variant_abs': string * typ * term -> string * term
     1.9    val fixedN: string
    1.10  end;
    1.11 @@ -237,6 +238,9 @@
    1.12  fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T;
    1.13  fun mark_bound x = mark_boundT (x, dummyT);
    1.14  
    1.15 +fun bound_vars vars body =
    1.16 +  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
    1.17 +
    1.18  fun strip_abss vars_of body_of tm =
    1.19    let
    1.20      val vars = vars_of tm;