# HG changeset patch
# User wenzelm
# Date 1721297288 -7200
# Node ID b1b53f6a08fa2f981b3ee1fd5208cbe985aab05c
# Parent  9a40ec7a202796024da642402b101be3caf86735
tuned;

diff -r 9a40ec7a2027 -r b1b53f6a08fa src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jul 18 11:36:09 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jul 18 12:08:08 2024 +0200
@@ -1341,9 +1341,10 @@
 
 fun unconstrainT_proof thy sorts_proof (ucontext: Logic.unconstrain_context) =
   let
+    val algebra = Sign.classes_of thy;
+
     val cache = zterm_cache thy;
     val typ_cache = typ_cache thy;
-    val algebra = Sign.classes_of thy;
 
     val typ =
       #apply (ZTypes.unsynchronized_cache