# HG changeset patch
# User wenzelm
# Date 1701947533 -3600
# Node ID 0bea00f77ba36bacfbf07ad6335c07a49b7a16e0
# Parent  377260b2824df207441073c2d65396d217861742
minor performance tuning: regular Same.operation;

diff -r 377260b2824d -r 0bea00f77ba3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 07 11:51:03 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 12:12:13 2023 +0100
@@ -646,7 +646,7 @@
 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 (incr_bv_same 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)) =
@@ -656,7 +656,7 @@
        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)
+       handle Same.SAME => prf % Same.map_option (incr_bv_same 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 377260b2824d -r 0bea00f77ba3 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Dec 07 11:51:03 2023 +0100
+++ b/src/Pure/term.ML	Thu Dec 07 12:12:13 2023 +0100
@@ -83,6 +83,7 @@
   val propT: typ
   val strip_all_body: term -> term
   val strip_all_vars: term -> (string * typ) list
+  val incr_bv_same: int -> int -> term Same.operation
   val incr_bv: int -> int -> term -> term
   val incr_boundvars: int -> term -> term
   val add_loose_bnos: term * int * int list -> int list
@@ -630,16 +631,21 @@
   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 =
-  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_bv_same inc =
+  if inc = 0 then fn _ => Same.same
+  else
+    let
+      fun term lev (Bound i) = if i >= lev then Bound (i + inc) else raise Same.SAME
+        | 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 incr_boundvars  0  t = t
-  | incr_boundvars inc t = incr_bv inc 0 t;
+fun incr_bv inc lev = Same.commit (incr_bv_same inc lev);
+
+fun incr_boundvars inc = incr_bv inc 0;
 
 (*Scan a pair of terms; while they are similar,
   accumulate corresponding bound vars in "al"*)