# HG changeset patch
# User wenzelm
# Date 1701787012 -3600
# Node ID 2933e71f4e094c9a88165af80bab5d9725f9731c
# Parent  b6f5d439238896720d1fca9a636ebf55b8fff7e6
clarified signature;

diff -r b6f5d4392388 -r 2933e71f4e09 src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Tue Dec 05 11:37:24 2023 +0100
+++ b/src/Pure/General/same.ML	Tue Dec 05 15:36:52 2023 +0100
@@ -12,6 +12,7 @@
   type 'a operation = ('a, 'a) function  (*exception SAME*)
   val same: ('a, 'b) function
   val commit: 'a operation -> 'a -> 'a
+  val commit_id: 'a operation -> 'a -> 'a * bool
   val function: ('a -> 'b option) -> ('a, 'b) function
   val map: 'a operation -> 'a list operation
   val map_option: ('a, 'b) function -> ('a option, 'b option) function
@@ -27,6 +28,7 @@
 
 fun same _ = raise SAME;
 fun commit f x = f x handle SAME => x;
+fun commit_id f x = (f x, false) handle SAME => (x, true);
 
 fun function f x =
   (case f x of
diff -r b6f5d4392388 -r 2933e71f4e09 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Tue Dec 05 11:37:24 2023 +0100
+++ b/src/Pure/term_subst.ML	Tue Dec 05 15:36:52 2023 +0100
@@ -120,7 +120,7 @@
       val substT = instantiateT_frees_same instT;
       fun subst (Const (c, T)) = Const (c, substT T)
         | subst (Free (x, T)) =
-            let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+            let val (T', same) = Same.commit_id substT T in
               (case Frees.lookup inst (x, T') of
                  SOME t' => t'
                | NONE => if same then raise Same.SAME else Free (x, T'))
@@ -168,7 +168,7 @@
     fun subst (Const (c, T)) = Const (c, substT T)
       | subst (Free (x, T)) = Free (x, substT T)
       | subst (Var ((x, i), T)) =
-          let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+          let val (T', same) = Same.commit_id substT T in
             (case Vars.lookup inst ((x, i), T') of
                SOME (t', j) => (maxify j; t')
              | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
@@ -191,7 +191,7 @@
     fun expand_head t =
       (case Term.head_of t of
         Var ((x, i), T) =>
-          let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+          let val (T', same) = Same.commit_id substT T in
             (case Vars.lookup inst ((x, i), T') of
               SOME (t', j) => (maxify j; SOME t')
             | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T'))))