# HG changeset patch
# User wenzelm
# Date 1701896282 -3600
# Node ID b3a6a8ec27efa5d5681372f19f0ae41c8398acff
# Parent  05cdedece5a9d96f466b39ed1864546330fdf9f7
tuned;

diff -r 05cdedece5a9 -r b3a6a8ec27ef src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 06 21:28:40 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 21:58:02 2023 +0100
@@ -515,7 +515,7 @@
 
 fun equal_intr_proof thy t u prf1 prf2 =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
@@ -523,7 +523,7 @@
 
 fun equal_elim_proof thy t u prf1 prf2 =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
@@ -630,7 +630,7 @@
 
 fun permute_prems_proof thy prems' j k prf =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val n = length prems';
   in
     mk_ZAbsP (map zterm prems')