# HG changeset patch
# User wenzelm
# Date 1701946114 -3600
# Node ID 4affbdbeefd459cb9e8955630523bc7bcd05c031
# Parent  46b621cf8aa715861871644591e388c4c8677012
clarified signature: more standard argument order;

diff -r 46b621cf8aa7 -r 4affbdbeefd4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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))
diff -r 46b621cf8aa7 -r 4affbdbeefd4 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- 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))
diff -r 46b621cf8aa7 -r 4affbdbeefd4 src/Pure/proofterm.ML
--- 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);
diff -r 46b621cf8aa7 -r 4affbdbeefd4 src/Pure/term.ML
--- 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"*)