--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 07 10:54:57 2023 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 07 11:48:34 2023 +0100
@@ -2228,7 +2228,7 @@
val step_body = recs |> map (repair_rec j)
|> List.foldl s_disj \<^Const>\<open>False\<close>
in
- (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
+ (fold_rev Term.abs (tl xs) (incr_bv ~1 j base_body)
|> ap_n_split (length arg_Ts) tuple_T bool_T,
Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
|> ap_n_split (length arg_Ts) tuple_T bool_T))
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Dec 07 10:54:57 2023 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Dec 07 11:48:34 2023 +0100
@@ -522,7 +522,7 @@
SOME (_, []) => \<^Const>\<open>True\<close>
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
- (incr_bv (~1, length ss + 1, arg_t))) ts)
+ (incr_bv ~1 (length ss + 1) arg_t)) ts)
| NONE =>
Const (\<^const_name>\<open>Ex\<close>, (T --> bool_T) --> bool_T)
$ Abs (s, T, kill ss Ts ts))
--- a/src/Pure/proofterm.ML Thu Dec 07 10:54:57 2023 +0100
+++ b/src/Pure/proofterm.ML Thu Dec 07 11:48:34 2023 +0100
@@ -643,12 +643,10 @@
inc is increment for bound variables
lev is level at which a bound variable is considered 'loose'*)
-fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
-
fun prf_incr_bv' incP _ Plev _ (PBound i) =
if i >= Plev then PBound (i+incP) else raise Same.SAME
| prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
- (AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t,
+ (AbsP (a, Same.map_option (same (op =) (incr_bv inct tlev)) t,
prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME =>
AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
| prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
@@ -657,8 +655,8 @@
(prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
| prf_incr_bv' incP inct Plev tlev (prf % t) =
- (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
- handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t)
+ (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv inct tlev) t
+ handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv inct tlev)) t)
| prf_incr_bv' _ _ _ _ _ = raise Same.SAME
and prf_incr_bv incP inct Plev tlev prf =
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf);
--- a/src/Pure/term.ML Thu Dec 07 10:54:57 2023 +0100
+++ b/src/Pure/term.ML Thu Dec 07 11:48:34 2023 +0100
@@ -83,7 +83,7 @@
val propT: typ
val strip_all_body: term -> term
val strip_all_vars: term -> (string * typ) list
- val incr_bv: int * int * term -> term
+ val incr_bv: int -> int -> term -> term
val incr_boundvars: int -> term -> term
val add_loose_bnos: term * int * int list -> int list
val loose_bnos: term -> int list
@@ -630,15 +630,16 @@
required when moving a term within abstractions
inc is increment for bound variables
lev is level at which a bound variable is considered 'loose'*)
-fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
- | incr_bv (inc, lev, Abs(a,T,body)) =
- Abs(a, T, incr_bv(inc,lev+1,body))
- | incr_bv (inc, lev, f$t) =
- incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
- | incr_bv (inc, lev, u) = u;
+fun incr_bv inc =
+ let
+ fun term lev (t as Bound i) = if i >= lev then Bound (i + inc) else t
+ | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
+ | term lev (t $ u) = term lev t $ term lev u
+ | term _ t = t;
+ in term end;
fun incr_boundvars 0 t = t
- | incr_boundvars inc t = incr_bv(inc,0,t);
+ | incr_boundvars inc t = incr_bv inc 0 t;
(*Scan a pair of terms; while they are similar,
accumulate corresponding bound vars in "al"*)