clarified -- avoid non-standard extend/merge;

--- a/src/Pure/Isar/code.ML	Fri Jul 17 17:06:54 2020 +0200
+++ b/src/Pure/Isar/code.ML	Fri Jul 17 19:10:24 2020 +0200
@@ -392,32 +392,42 @@
 local
 
 type data = Any.T Datatab.table;
-fun empty_dataref () = Synchronized.var "code data" (NONE : (data * Context.theory_id) option);
+
+fun make_dataref thy =
+  (Context.theory_long_name thy,
+    Synchronized.var "code data" (NONE : (data * Context.theory_id) option));
 
 structure Code_Data = Theory_Data
 (
-  type T = specs * (data * Context.theory_id) option Synchronized.var;
-  val empty = (empty_specs, empty_dataref ());
-  val extend : T -> T = apsnd (K (empty_dataref ()));
-  fun merge ((specs1, _), (specs2, _)) =
-    (merge_specs (specs1, specs2), empty_dataref ());
+  type T = specs * (string * (data * Context.theory_id) option Synchronized.var);
+  val empty = (empty_specs, make_dataref (Context.the_global_context ()));
+  val extend = I;
+  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)
+
 in
 
+val _ = Theory.setup (Theory.at_begin init_dataref);
+
 
 (* access to executable specifications *)
 
 val specs_of : theory -> specs = fst o Code_Data.get;
 
-fun modify_specs f = Code_Data.map (fn (specs, _) => (f specs, empty_dataref ()));
+fun modify_specs f thy =
+  Code_Data.map (fn (specs, _) => (f specs, make_dataref thy)) thy;
 
 
 (* access to data dependent on executable specifications *)
 
 fun change_yield_data (kind, mk, dest) theory f =
   let
-    val dataref = (snd o Code_Data.get) theory;
+    val dataref = #2 (#2 (Code_Data.get theory));
     val (datatab, thy_id) = case Synchronized.value dataref
      of SOME (datatab, thy_id) =>
         if Context.eq_thy_id (Context.theory_id theory, thy_id)

--- a/src/Tools/Code/code_target.ML	Fri Jul 17 17:06:54 2020 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Jul 17 19:10:24 2020 +0200
@@ -186,16 +186,18 @@
 (
   type T = (target * Code_Printer.data) Symtab.table * int;
   val empty = (Symtab.empty, 0);
-  fun extend (targets, _) = (targets, 0);
-  fun merge ((targets1, _), (targets2, _)) : T =
-    let val targets' =
-      Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
-        if #serial target1 = #serial target2 then
-        ({serial = #serial target1, language = #language target1,
-          ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
-          Code_Printer.merge_data (data1, data2))
-        else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2)
-    in (targets', 0) end;
+  val extend = I;
+  fun merge ((targets1, index1), (targets2, index2)) : T =
+    let
+      val targets' =
+        Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
+          if #serial target1 = #serial target2 then
+          ({serial = #serial target1, language = #language target1,
+            ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
+            Code_Printer.merge_data (data1, data2))
+          else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2)
+      val index' = Int.max (index1, index2);
+    in (targets', index') end;
 );
 
 val exists_target = Symtab.defined o #1 o Targets.get;
@@ -205,6 +207,12 @@
   then target_name
   else error ("Unknown code target language: " ^ quote target_name);
 
+fun reset_index thy =
+  if #2 (Targets.get thy) = 0 then NONE
+  else SOME ((Targets.map o apsnd) (K 0) thy);
+
+val _ = Theory.setup (Theory.at_begin reset_index);
+
 fun next_export thy =
   let
     val thy' = (Targets.map o apsnd) (fn i => i + 1) thy;