# HG changeset patch
# User wenzelm
# Date 1702062532 -3600
# Node ID 58f9b0d53d97aea0e5f8777bd8c42eb7ed4de782
# Parent  1089a1f47d0a76c04de103bfec47f2c119249bbd
tuned;

diff -r 1089a1f47d0a -r 58f9b0d53d97 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Dec 08 19:52:24 2023 +0100
+++ b/src/Pure/logic.ML	Fri Dec 08 20:08:52 2023 +0100
@@ -450,7 +450,7 @@
       (fn TVar ((a, i), S) => TVar ((a, i + k), S)
         | _ => raise Same.SAME);
 
-fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
+fun incr_tvar k = Same.commit (incr_tvar_same k);
 
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
@@ -476,7 +476,7 @@
           | incr _ (Bound _) = raise Same.SAME;
       in incr 0 end;
 
-fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
+fun incr_indexes arg = Same.commit (incr_indexes_same arg);
 
 
 (* Lifting functions from subgoal and increment: