tuned signature;

--- a/src/Pure/General/table.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/General/table.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -68,6 +68,7 @@
   val make_set: key list -> set
   type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
+  val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -610,6 +611,8 @@
     fun total_size () = size (! cache1) + size (! cache2);
   in {apply = apply, reset = reset, size = total_size} end;
 
+fun apply_unsynchronized_cache f = #apply (unsynchronized_cache f);
+
 
 (* ML pretty-printing *)
 

--- a/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -65,15 +65,14 @@
   Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity_cache ctxt =
-  Symtab.unsynchronized_cache (fn c =>
+  Symtab.apply_unsynchronized_cache (fn c =>
     Syntax.get_consts (Proof_Context.syntax_of ctxt) c
     |> maps (Lexicon.unmark
        {case_class = markup_class ctxt,
         case_type = markup_type ctxt,
         case_const = markup_const ctxt,
         case_fixed = markup_free ctxt,
-        case_default = K []}))
-  |> #apply;
+        case_default = K []}));
 
 
 
@@ -267,8 +266,8 @@
 
 fun decode_term ctxt =
   let
-    val markup_free_cache = #apply (Symtab.unsynchronized_cache (markup_free ctxt));
-    val markup_const_cache = #apply (Symtab.unsynchronized_cache (markup_const ctxt));
+    val markup_free_cache = Symtab.apply_unsynchronized_cache (markup_free ctxt);
+    val markup_const_cache = Symtab.apply_unsynchronized_cache (markup_const ctxt);
 
     fun decode (result as (_: Position.report_text list, Exn.Exn _)) = result
       | decode (reports0, Exn.Res tm) =
@@ -714,7 +713,7 @@
 local
 
 fun extern_cache ctxt =
-  Symtab.unsynchronized_cache (fn c =>
+  Symtab.apply_unsynchronized_cache (fn c =>
     (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of
       [b] => b
     | bs =>
@@ -722,18 +721,16 @@
           [] => c
         | [b] => b
         | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs)))
-    |> Proof_Context.extern_entity ctxt)
-  |> #apply;
+    |> Proof_Context.extern_entity ctxt);
 
 val var_or_skolem_cache =
-  Symtab.unsynchronized_cache (fn s =>
+  Symtab.apply_unsynchronized_cache (fn s =>
     (case Lexicon.read_variable s of
       SOME (x, i) =>
         (case try Name.dest_skolem x of
           SOME x' => (Markup.skolem, Term.string_of_vname (x', i))
         | NONE => (Markup.var, s))
-    | NONE => (Markup.var, s)))
-  |> #apply;
+    | NONE => (Markup.var, s)));
 
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
@@ -751,8 +748,8 @@
     val extern = extern_cache ctxt;
 
     val free_or_skolem_cache =
-      Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, Proof_Context.extern_fixed ctxt x))
-      |> #apply;
+      Symtab.apply_unsynchronized_cache (fn x =>
+        (markup_free ctxt x, Proof_Context.extern_fixed ctxt x));
 
     val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
     val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);

--- a/src/Pure/term_items.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/term_items.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -36,6 +36,7 @@
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
   type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
+  val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -89,6 +90,7 @@
 
 type 'a cache_ops = 'a Table.cache_ops;
 val unsynchronized_cache = Table.unsynchronized_cache;
+val apply_unsynchronized_cache = Table.apply_unsynchronized_cache;
 
 
 (* set with order of addition *)

--- a/src/Pure/thm.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/thm.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -1095,8 +1095,8 @@
                 SOME T' => T'
               | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
         val map_ztyp =
-          #apply (ZTypes.unsynchronized_cache
-            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
+          ZTypes.apply_unsynchronized_cache
+            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
 
         val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
         val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;

--- a/src/Pure/zterm.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -548,7 +548,7 @@
 
 fun instantiate_type_same instT =
   if ZTVars.is_empty instT then Same.same
-  else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
+  else ZTypes.apply_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));
@@ -863,9 +863,7 @@
   let
     val lookup =
       if Vartab.is_empty tenv then K NONE
-      else
-        #apply (ZVars.unsynchronized_cache
-          (apsnd typ_of #> Envir.lookup envir #> Option.map zterm));
+      else ZVars.apply_unsynchronized_cache (apsnd typ_of #> Envir.lookup envir #> Option.map zterm);
 
     val normT = norm_type_same ztyp tyenv;
 
@@ -1008,8 +1006,8 @@
     val typ_operation = #typ_operation ucontext {strip_sorts = true};
     val unconstrain_typ = Same.commit typ_operation;
     val unconstrain_ztyp =
-      #apply (ZTypes.unsynchronized_cache
-        (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
+      ZTypes.apply_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);
 
@@ -1226,10 +1224,10 @@
     val typ =
       if Names.is_empty tfrees then Same.same
       else
-        #apply (ZTypes.unsynchronized_cache
+        ZTypes.apply_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)
@@ -1251,10 +1249,10 @@
     let
       val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
       val typ =
-        #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+        ZTypes.apply_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 =
@@ -1263,7 +1261,7 @@
   | SOME f =>
       let
         val tvar = ztyp_of o Same.function f;
-        val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
+        val typ = ZTypes.apply_unsynchronized_cache (subst_type_same tvar);
       in map_proof_types {hyps = false} typ prf end);
 
 
@@ -1297,7 +1295,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 #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
+    in ZTypes.apply_unsynchronized_cache (subst_type_same tvar) end;
 
 fun incr_indexes_proof inc prf =
   let
@@ -1437,8 +1435,8 @@
     val typ_cache = typ_cache thy;
 
     val typ =
-      #apply (ZTypes.unsynchronized_cache
-        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
+      ZTypes.apply_unsynchronized_cache
+        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
 
     val typ_sort = #typ_operation ucontext {strip_sorts = false};