--- a/src/Pure/Syntax/syn_trans.ML Sat Mar 26 10:52:29 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Sat Mar 26 12:01:40 2011 +0100
@@ -10,6 +10,7 @@
val eta_contract_raw: Config.raw
val eta_contract: bool Config.T
val atomic_abs_tr': string * typ * term -> term * term
+ val const_abs_tr': term -> term
val mk_binder_tr: string * string -> string * (term list -> term)
val mk_binder_tr': string * string -> string * (term list -> term)
val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
@@ -316,6 +317,13 @@
([], _) => raise Ast.AST ("abs_ast_tr'", asts)
| (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
+fun const_abs_tr' t =
+ (case eta_abs t of
+ Abs (_, _, t') =>
+ if Term.is_dependent t' then raise Match
+ else incr_boundvars ~1 t'
+ | _ => raise Match);
+
(* binders *)