# HG changeset patch
# User wenzelm
# Date 1701864247 -3600
# Node ID a9c55fef42b0d854575dec3f7cc5aea25c953d53
# Parent  42ca72f06632b2f6136dacb775220e20156c1947
tuned signature;

diff -r 42ca72f06632 -r a9c55fef42b0 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 06 10:29:37 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 13:04:07 2023 +0100
@@ -233,31 +233,31 @@
       | term (ZClass (T, c)) = ZClass (typ T, c);
   in term end;
 
+fun map_insts_same typ term (instT, inst) =
+  let
+    val changed = Unsynchronized.ref false;
+    val instT' =
+      (instT, instT) |-> ZTVars.fold (fn (v, T) =>
+        (case Same.catch typ T of
+          SOME U => (changed := true; ZTVars.update (v, U))
+        | NONE => I));
+    val inst' =
+      if ! changed then
+        ZVars.dest inst
+        |> map (fn ((x, T), t) => ((x, Same.commit typ T), Same.commit term t))
+        |> ZVars.make
+      else
+        (inst, inst) |-> ZVars.fold (fn (v, t) =>
+          (case Same.catch term t of
+            SOME u => (changed := true; ZVars.update (v, u))
+          | NONE => I));
+  in if ! changed then (instT', inst') else raise Same.SAME end;
+
 fun map_proof_same typ term =
   let
-    fun change_insts (instT, inst) =
-      let
-        val changed = Unsynchronized.ref false;
-        val instT' =
-          (instT, instT) |-> ZTVars.fold (fn (v, T) =>
-            (case Same.catch typ T of
-              SOME U => (changed := true; ZTVars.update (v, U))
-            | NONE => I));
-        val inst' =
-          if ! changed then
-            ZVars.dest inst
-            |> map (fn ((x, T), t) => ((x, Same.commit typ T), Same.commit term t))
-            |> ZVars.make
-          else
-            (inst, inst) |-> ZVars.fold (fn (v, t) =>
-              (case Same.catch term t of
-                SOME u => (changed := true; ZVars.update (v, u))
-              | NONE => I));
-      in if ! changed then SOME (instT', inst') else NONE end;
-
     fun proof ZDummy = raise Same.SAME
       | proof (ZConstP (a, A, instT, inst)) =
-          (case change_insts (instT, inst) of
+          (case Same.catch (map_insts_same typ term) (instT, inst) of
             NONE => ZConstP (a, term A, instT, inst)
           | SOME (instT', inst') => ZConstP (a, Same.commit term A, instT', inst'))
       | proof (ZBoundP _) = raise Same.SAME