# HG changeset patch
# User wenzelm
# Date 1684155877 -7200
# Node ID 64f81d011a90d0338ec8e8bf3c5acca9c8ce0c06
# Parent  92d487a28545a8e47d019667079d319b5a801574
clarified signature: avoid convoluted operations;

diff -r 92d487a28545 -r 64f81d011a90 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon May 15 14:34:38 2023 +0200
+++ b/src/Pure/Isar/code.ML	Mon May 15 15:04:37 2023 +0200
@@ -393,21 +393,23 @@
 
 type data = Any.T Datatab.table;
 
-fun make_dataref thy =
-  (Context.theory_long_name thy,
-    Synchronized.var "code data" (NONE : (data * Context.theory_id) option));
+fun make_dataref () =
+  Synchronized.var "code data" (NONE : (data * Context.theory_id) option);
 
 structure Code_Data = Theory_Data
 (
   type T = specs * (string * (data * Context.theory_id) option Synchronized.var);
-  val empty = (empty_specs, make_dataref (Context.the_global_context ()));
+  val empty =
+    (empty_specs, (Context.theory_long_name (Context.the_global_context ()), make_dataref ()));
   fun merge ((specs1, dataref), (specs2, _)) =
     (merge_specs (specs1, specs2), dataref);
 );
 
 fun init_dataref thy =
-  if #1 (#2 (Code_Data.get thy)) = Context.theory_long_name thy then NONE
-  else SOME ((Code_Data.map o apsnd) (fn _ => make_dataref thy) thy)
+  let val thy_name = Context.theory_long_name thy in
+    if #1 (#2 (Code_Data.get thy)) = thy_name then NONE
+    else SOME ((Code_Data.map o apsnd) (K (thy_name, make_dataref ())) thy)
+  end;
 
 in
 
@@ -419,7 +421,8 @@
 val specs_of : theory -> specs = fst o Code_Data.get;
 
 fun modify_specs f thy =
-  Code_Data.map (fn (specs, _) => (f specs, make_dataref thy)) thy;
+  let val thy_name = Context.theory_long_name thy
+  in Code_Data.map (fn (specs, _) => (f specs, (thy_name, make_dataref ()))) thy end;
 
 
 (* access to data dependent on executable specifications *)