added variant_abs (from term.ML);
authorwenzelm
Tue Jul 25 21:18:09 2006 +0200 (2006-07-25)
changeset 2020287205ea2af06
parent 20201 24b49cbd438b
child 20203 914433927687
added variant_abs (from term.ML);
tuned;
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 25 21:18:08 2006 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 25 21:18:09 2006 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val mark_bound: string -> term
     1.5    val mark_boundT: string * typ -> term
     1.6    val bound_vars: (string * typ) list -> term -> term
     1.7 +  val variant_abs: string * typ * term -> string * term
     1.8    val variant_abs': string * typ * term -> string * term
     1.9  end;
    1.10  
    1.11 @@ -383,10 +384,12 @@
    1.12  
    1.13  (* dependent / nondependent quantifiers *)
    1.14  
    1.15 -fun variant_abs' (x, T, b) =
    1.16 -  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) in
    1.17 -    (x', subst_bound (mark_boundT (x', T), b))
    1.18 -  end;
    1.19 +fun var_abs mark (x, T, b) =
    1.20 +  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
    1.21 +  in (x', subst_bound (mark (x', T), b)) end;
    1.22 +
    1.23 +val variant_abs = var_abs Free;
    1.24 +val variant_abs' = var_abs mark_boundT;
    1.25  
    1.26  fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
    1.27        if Term.loose_bvar1 (B, 0) then