--- a/src/Pure/term.ML Fri Dec 08 14:35:24 2023 +0100
+++ b/src/Pure/term.ML Fri Dec 08 14:48:17 2023 +0100
@@ -90,6 +90,7 @@
val loose_bnos: term -> int list
val loose_bvar: term * int -> bool
val loose_bvar1: term * int -> bool
+ val subst_bounds_same: term list -> int -> term Same.operation
val subst_bounds: term list * term -> term
val subst_bound: term * term -> term
val betapply: term * term -> term
@@ -704,19 +705,24 @@
Loose bound variables >=n are reduced by "n" to
compensate for the disappearance of lambdas.
*)
+fun subst_bounds_same args =
+ if null args then fn _ => Same.same
+ else
+ let
+ val n = length args;
+ fun term lev (Bound i) =
+ (if i < lev then raise Same.SAME (*var is locally bound*)
+ else if i - lev < n then incr_boundvars lev (nth args (i - lev))
+ else Bound (i - n)) (*loose: change it*)
+ | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
+ | term lev (t $ u) =
+ (term lev t $ Same.commit (term lev) u
+ handle Same.SAME => t $ term lev u)
+ | term _ _ = raise Same.SAME;
+ in term end;
+
fun subst_bounds (args: term list, body) : term =
- let
- val n = length args;
- fun term lev (Bound i) =
- (if i < lev then raise Same.SAME (*var is locally bound*)
- else if i - lev < n then incr_boundvars lev (nth args (i - lev))
- else Bound (i - n)) (*loose: change it*)
- | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
- | term lev (t $ u) =
- (term lev t $ Same.commit (term lev) u
- handle Same.SAME => t $ term lev u)
- | term _ _ = raise Same.SAME;
- in if null args then body else Same.commit (term 0) body end;
+ if null args then body else Same.commit (subst_bounds_same args 0) body;
(*Special case: one argument*)
fun subst_bound (arg, body) : term =