# HG changeset patch
# User wenzelm
# Date 1681997194 -7200
# Node ID 186bd4012b7835fe6c43d4267fbe07051b044637
# Parent  dfc1db3f0fcbbd8b21a4d2303f9393ea6ff91f3b
tuned;

diff -r dfc1db3f0fcb -r 186bd4012b78 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Apr 20 15:24:31 2023 +0200
+++ b/src/Pure/context.ML	Thu Apr 20 15:26:34 2023 +0200
@@ -282,13 +282,18 @@
 fun invoke_empty k = invoke "" (K o #empty) k ();
 fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
 
-fun declare_theory_data pos empty merge =
+fun declare_data pos empty merge =
   let
     val k = serial ();
     val kind = {pos = pos, empty = empty, merge = merge};
     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   in k end;
 
+fun get_data k thy =
+  (case Datatab.lookup (data_of thy) k of
+    SOME x => x
+  | NONE => invoke_empty k);
+
 fun merge_data thys = Datatab.join (invoke_merge thys);
 
 end;
@@ -452,14 +457,11 @@
 structure Theory_Data =
 struct
 
-val declare = declare_theory_data;
+val declare = declare_data;
 
-fun get k dest thy =
-  (case Datatab.lookup (data_of thy) k of
-    SOME x => x
-  | NONE => invoke_empty k) |> dest;
+fun get k dest thy = dest (get_data k thy);
 
-fun put k mk x = update_thy (Datatab.update (k, mk x));
+fun put k make x = update_thy (Datatab.update (k, make x));
 
 fun sizeof1 k thy =
   Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1;
@@ -532,8 +534,8 @@
     SOME x => x
   | NONE => init_fallback k thy) |> dest;
 
-fun put k mk x (Proof.Context (data, thy)) =
-  Proof.Context (Datatab.update (k, mk x) data, thy);
+fun put k make x (Proof.Context (data, thy)) =
+  Proof.Context (Datatab.update (k, make x) data, thy);
 
 end;