# HG changeset patch
# User wenzelm
# Date 1701347717 -3600
# Node ID 58bb68b9470fd08ff92103f647136be4120e5d31
# Parent  6c5ca8f04d60956edb4646cdec052a6c932eea29
tuned;

diff -r 6c5ca8f04d60 -r 58bb68b9470f src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Nov 30 13:25:06 2023 +0100
+++ b/src/Pure/General/table.ML	Thu Nov 30 13:35:17 2023 +0100
@@ -164,16 +164,16 @@
 
 fun map_table f =
   let
+    fun apply (k, x) = (k, f k x);
+
     fun map Empty = Empty
-      | map (Leaf1 (k, x)) = Leaf1 (k, f k x)
-      | map (Leaf2 ((k1, x1), (k2, x2))) =
-          Leaf2 ((k1, f k1 x1), (k2, f k2 x2))
-      | map (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
-          Leaf3 ((k1, f k1 x1), (k2, f k2 x2), (k3, f k3 x3))
-      | map (Branch2 (left, (k, x), right)) =
-          Branch2 (map left, (k, f k x), map right)
-      | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-          Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right)
+      | map (Leaf1 e) = Leaf1 (apply e)
+      | map (Leaf2 (e1, e2)) = Leaf2 (apply e1, apply e2)
+      | map (Leaf3 (e1, e2, e3)) = Leaf3 (apply e1, apply e2, apply e3)
+      | map (Branch2 (left, e, right)) =
+          Branch2 (map left, apply e, map right)
+      | map (Branch3 (left, e1, mid, e2, right)) =
+          Branch3 (map left, apply e1, map mid, apply e2, map right)
       | map (Size (m, arg)) = Size (m, map arg);
   in map end;
 
@@ -430,11 +430,11 @@
 
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE Empty = raise Match
-  | del NONE (Leaf1 p) = (p, (true, Empty))
+  | del NONE (Leaf1 e) = (e, (true, Empty))
   | del NONE (Leaf2 (e1, e2)) = (e1, (false, Leaf1 e2))
-  | del k (Leaf1 p) =
-      (case compare k p of
-        EQUAL => (p, (true, Empty))
+  | del k (Leaf1 e) =
+      (case compare k e of
+        EQUAL => (e, (true, Empty))
       | _ => raise UNDEF (the k))
   | del k (Leaf2 (e1, e2)) =
       (case compare k e1 of