# HG changeset patch
# User wenzelm
# Date 1702042524 -3600
# Node ID 5d27271701a2ebc50b72f8eb555762f73fdbdac8
# Parent  f6bbe80f5f414114cdd6462782469d395bdca5a1
tuned;

diff -r f6bbe80f5f41 -r 5d27271701a2 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Dec 08 14:27:42 2023 +0100
+++ b/src/Pure/zterm.ML	Fri Dec 08 14:35:24 2023 +0100
@@ -390,6 +390,8 @@
   | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
   | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
 
+fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
 fun term_of_consts consts =
   let
     val instance = Consts.instance consts;
@@ -435,7 +437,7 @@
   else
     let
       val {ztyp, zterm} = zterm_cache_consts consts;
-      val typ = ZTypes.unsynchronized_cache typ_of;
+      val typ = typ_cache ();
 
       val lookup =
         if Vartab.is_empty tenv then K NONE
@@ -466,7 +468,7 @@
 in
 
 fun norm_type tyenv =
-  Same.commit (norm_type_same (Typtab.unsynchronized_cache ztyp_of) tyenv);
+  Same.commit (norm_type_same (ztyp_cache ()) tyenv);
 
 fun norm_term_consts consts envir =
   Same.commit (norm_term_same consts envir);