src/Pure/zterm.ML

--- a/src/Pure/zterm.ML	Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/zterm.ML	Mon Jul 15 12:26:15 2024 +0200
@@ -470,7 +470,7 @@
 
 fun instantiate_type_same instT =
   if ZTVars.is_empty instT then Same.same
-  else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
+  else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
 
 fun instantiate_term_same typ inst =
   subst_term_same typ (Same.function (ZVars.lookup inst));
@@ -587,7 +587,7 @@
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
-fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+fun ztyp_cache () = #apply (Typtab.unsynchronized_cache ztyp_of);
 
 fun zterm_cache thy =
   let
@@ -622,7 +622,7 @@
   | 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 typ_cache () = #apply (ZTypes.unsynchronized_cache typ_of);
 
 fun term_of thy =
   let
@@ -721,7 +721,7 @@
   let
     val lookup =
       if Vartab.is_empty tenv then K NONE
-      else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+      else #apply (ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm));
 
     val normT = norm_type_same ztyp tyenv;
 
@@ -870,7 +870,8 @@
     val typ_operation = #typ_operation ucontext {strip_sorts = true};
     val unconstrain_typ = Same.commit typ_operation;
     val unconstrain_ztyp =
-      ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
+      #apply (ZTypes.unsynchronized_cache
+        (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
     val unconstrain_zterm = zterm o Term.map_types typ_operation;
     val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp);
 
@@ -1087,10 +1088,10 @@
     val typ =
       if Names.is_empty tfrees then Same.same
       else
-        ZTypes.unsynchronized_cache
+        #apply (ZTypes.unsynchronized_cache
           (subst_type_same (fn ((a, i), S) =>
             if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
-            else raise Same.SAME));
+            else raise Same.SAME)));
     val term =
       subst_term_same typ (fn ((x, i), T) =>
         if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
@@ -1112,10 +1113,10 @@
     let
       val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
       val typ =
-        ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+        #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
-          | SOME w => ZTVar w)));
+          | SOME w => ZTVar w))));
     in map_proof_types {hyps = false} typ prf end;
 
 fun legacy_freezeT_proof t prf =
@@ -1124,7 +1125,7 @@
   | SOME f =>
       let
         val tvar = ztyp_of o Same.function f;
-        val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
+        val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
       in map_proof_types {hyps = false} typ prf end);
 
 
@@ -1158,7 +1159,7 @@
   if inc = 0 then Same.same
   else
     let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME
-    in ZTypes.unsynchronized_cache (subst_type_same tvar) end;
+    in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
 
 fun incr_indexes_proof inc prf =
   let
@@ -1296,8 +1297,8 @@
     val algebra = Sign.classes_of thy;
 
     val typ =
-      ZTypes.unsynchronized_cache
-        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
+      #apply (ZTypes.unsynchronized_cache
+        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
 
     val typ_sort = #typ_operation ucontext {strip_sorts = false};