--- 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
--- 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'))))