# HG changeset patch
# User wenzelm
# Date 1682151761 -7200
# Node ID 9c5e8460df059c65bbe152eb33c3cba2efcf8d3d
# Parent  89676df5846a73fd5611b949457c924642675f54# Parent  acee6c7fafff799aeefb69b5b44b51e8923c5556
merged

diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Analysis/measurable.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -34,82 +34,73 @@
 structure Measurable : MEASURABLE =
 struct
 
-type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
+type preprocessor = thm -> Proof.context -> thm list * Proof.context
 
 datatype level = Concrete | Generic;
 
-fun eq_measurable_thms ((th1, d1), (th2, d2)) = 
+type measurable_thm = thm * (bool * level);
+
+fun eq_measurable_thm ((th1, d1): measurable_thm, (th2, d2): measurable_thm) =
   d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
 
-fun merge_dups (xs:(string * preprocessor) list) ys =
-  xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) 
+fun merge_preprocessors (xs: (string * preprocessor) list, ys) =
+  xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys)
 
 structure Data = Generic_Data
 (
-  type T = {
-    measurable_thms : (thm * (bool * level)) Item_Net.T,
-    dest_thms : thm Item_Net.T,
-    cong_thms : thm Item_Net.T,
-    preprocessors : (string * preprocessor) list }
-  val empty: T = {
-    measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
-    dest_thms = Thm.item_net,
-    cong_thms = Thm.item_net,
-    preprocessors = [] };
-  fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
-      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
-    measurable_thms = Item_Net.merge (t1, t2),
-    dest_thms = Item_Net.merge (dt1, dt2),
-    cong_thms = Item_Net.merge (ct1, ct2),
-    preprocessors = merge_dups i1 i2 
-    };
+  type T =
+    measurable_thm Item_Net.T *
+    (*dest_thms*) thm Item_Net.T *
+    (*cong_thms*) thm Item_Net.T *
+    (string * preprocessor) list
+  val empty: T =
+    (Item_Net.init eq_measurable_thm (single o Thm.full_prop_of o fst), Thm.item_net, Thm.item_net, [])
+  fun merge
+   ((measurable_thms1, dest_thms1, cong_thms1, preprocessors1),
+    (measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T =
+   (Item_Net.merge (measurable_thms1, measurable_thms2),
+    Item_Net.merge (dest_thms1, dest_thms2),
+    Item_Net.merge (cong_thms1, cong_thms2),
+    merge_preprocessors (preprocessors1, preprocessors2))
 );
 
-val debug =
-  Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false)
-
-val split =
-  Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true)
+val map_measurable_thms = Data.map o @{apply 4(1)}
+val map_dest_thms = Data.map o @{apply 4(2)}
+val map_cong_thms = Data.map o @{apply 4(3)}
+val map_preprocessors = Data.map o @{apply 4(4)}
 
-fun map_data f1 f2 f3 f4
-  {measurable_thms = t1,    dest_thms = t2,    cong_thms = t3,    preprocessors = t4 } =
-  {measurable_thms = f1 t1, dest_thms = f2 t2, cong_thms = f3 t3, preprocessors = f4 t4}
-
-fun map_measurable_thms f = map_data f I I I
-fun map_dest_thms f = map_data I f I I
-fun map_cong_thms f = map_data I I f I
-fun map_preprocessors f = map_data I I I f
+val debug = Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false)
+val split = Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true)
 
 fun generic_add_del map : attribute context_parser =
   Scan.lift
     (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
-    (fn f => Thm.declaration_attribute (Data.map o map o f))
+    (fn f => Thm.declaration_attribute (map o f o Thm.trim_context))
 
 val dest_thm_attr = generic_add_del map_dest_thms
-
 val cong_thm_attr = generic_add_del map_cong_thms
 
 fun del_thm th net =
   let
-    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
+    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm_prop (th, th'))
   in fold Item_Net.remove thms net end ;
 
 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
-  (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm))
-
-val get_dest = Item_Net.content o #dest_thms o Data.get;
+  (map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm) o Thm.trim_context)
 
-val get_cong = Item_Net.content o #cong_thms o Data.get;
-val add_cong = Data.map o map_cong_thms o Item_Net.update;
-val del_cong = Data.map o map_cong_thms o Item_Net.remove;
+fun get_dest context = map (Thm.transfer'' context) (Item_Net.content (#2 (Data.get context)));
+fun get_cong context = map (Thm.transfer'' context) (Item_Net.content (#3 (Data.get context)));
+
+val add_cong = map_cong_thms o Item_Net.update o Thm.trim_context;
+val del_cong = map_cong_thms o Item_Net.remove o Thm.trim_context;
 fun add_del_cong_thm true = add_cong
   | add_del_cong_thm false = del_cong
 
-fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)]))
-fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name)))
+fun add_preprocessor name f = map_preprocessors (fn xs => xs @ [(name, f)])
+fun del_preprocessor name = map_preprocessors (filter (fn (n, _) => n <> name))
 val add_local_cong = Context.proof_map o add_cong
 
-val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ;
+val get_preprocessors = Context.Proof #> Data.get #> #4;
 
 fun is_too_generic thm =
   let 
@@ -117,9 +108,10 @@
     val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   in is_Var (head_of concl') end
 
-val get_thms = Data.get #> #measurable_thms #> Item_Net.content ;
+fun get_thms context =
+  map (apfst (Thm.transfer'' context)) (Item_Net.content (#1 (Data.get context)));
 
-val get_all = get_thms #> map fst ;
+val get_all = get_thms #> map fst;
 
 fun debug_tac ctxt msg f =
   if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Library/refute.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -2375,7 +2375,7 @@
                               val result = fold (fn arg_i => fn i =>
                                 interpretation_apply (i, arg_i)) arg_intrs intr
                               (* update 'REC_OPERATORS' *)
-                              val _ = Array.update (arr, elem, (true, result))
+                              val _ = Array.upd arr elem (true, result)
                             in
                               result
                             end
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -239,7 +239,7 @@
   let val consts = Term.add_const_names (Thm.prop_of th) [] in
     exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
     exists (member (op =) forbidden_consts) consts orelse
-    length (Long_Name.explode s) <> 2 orelse
+    Long_Name.count s <> 2 orelse
     String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
     String.isSuffix "_def" s orelse
     String.isSuffix "_raw" s orelse
@@ -331,7 +331,7 @@
 
 fun thms_of all thy =
   filter
-    (fn th => (all orelse Thm.theory_name th = Context.theory_name thy)
+    (fn th => (all orelse Thm.theory_long_name th = Context.theory_long_name thy)
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
 
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Apr 22 10:22:41 2023 +0200
@@ -144,7 +144,7 @@
 val mono_timeout = seconds 1.0
 
 fun is_forbidden_theorem name =
-  length (Long_Name.explode name) <> 2 orelse
+  Long_Name.count name <> 2 orelse
   String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
   String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
   String.isSuffix "_def" name orelse
@@ -153,7 +153,7 @@
 fun theorems_of thy =
   filter (fn (name, th) =>
              not (is_forbidden_theorem name) andalso
-             Thm.theory_name th = Context.theory_name thy)
+             Thm.theory_long_name th = Context.theory_long_name thy)
          (Global_Theory.all_thms_of thy true)
 
 fun check_formulas tsp =
@@ -175,7 +175,7 @@
 
 fun check_theory thy =
   let
-    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
+    val path = File.tmp_path (Context.theory_base_name thy ^ ".out" |> Path.explode)
     val _ = File.write path ""
     fun check_theorem (name, th) =
       let
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/TPTP/mash_export.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -58,7 +58,7 @@
   | _ => ("", []))
 
 fun has_thm_thy th thy =
-  Context.theory_name thy = Thm.theory_name th
+  Context.theory_base_name thy = Thm.theory_base_name th
 
 fun has_thys thys th = exists (has_thm_thy th) thys
 
@@ -98,7 +98,7 @@
     fun do_fact ((_, stature), th) =
       let
         val name = nickname_of_thm th
-        val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+        val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
         val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
       in
         File.append path s
@@ -187,14 +187,14 @@
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val isar_deps = isar_dependencies_of name_tabs th
           val do_query = not (is_bad_query ctxt step j th isar_deps)
-          val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+          val goal_feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
           val access_facts = filter_accessible_from th new_facts @ old_facts
           val (marker, deps) =
             smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
 
           fun extra_features_of (((_, stature), th), weight) =
             [Thm.prop_of th]
-            |> features_of ctxt (Thm.theory_name th) stature
+            |> features_of ctxt (Thm.theory_base_name th) stature
             |> map (rpair (weight * extra_feature_factor))
 
           val query =
@@ -261,7 +261,7 @@
               val suggs =
                 old_facts
                 |> filter_accessible_from th
-                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th)
+                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_base_name th)
                   params max_suggs hyp_ts concl_t
                 |> map (nickname_of_thm o snd)
             in
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -16,7 +16,7 @@
 
 fun thms_of thy thy_name =
   Global_Theory.all_thms_of thy false
-  |> filter (fn (_, th) => Thm.theory_name th = thy_name)
+  |> filter (fn (_, th) => Thm.theory_base_name th = thy_name)
 
 fun do_while P f s list =
   if P s then
@@ -71,7 +71,7 @@
     val thy = Proof_Context.theory_of ctxt
     val all_thms =
       thms_of thy thy_name
-      |> filter (fn (name, _) => length (Long_Name.explode name) = 2)  (* FIXME !? *)
+      |> filter (fn (name, _) => Long_Name.count name = 2)  (* FIXME !? *)
       |> sort_by #1
     val check = check_unused_assms ctxt
   in rev (Par_List.map check all_thms) end
@@ -95,7 +95,8 @@
 
 fun print_unused_assms ctxt opt_thy_name =
   let
-    val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
+    val thy_name =
+      the_default (Context.theory_base_name (Proof_Context.theory_of ctxt)) opt_thy_name
     val results = find_unused_assms ctxt thy_name
     val total = length results
     val with_assumptions = length (filter (is_some o snd) results)
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -484,7 +484,7 @@
           let
             val n = length ths
             val collection = n > 1
-            val dotted_name = length (Long_Name.explode name0) > 2 (* ignore theory name *)
+            val dotted_name = Long_Name.count name0 > 2 (* ignore theory name *)
 
             fun check_thms a =
               (case try (Proof_Context.get_thms ctxt) a of
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -796,7 +796,7 @@
       (* There must be a better way to detect local facts. *)
       (case Long_Name.dest_local hint of
         SOME suf =>
-        Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
+        Long_Name.implode [Thm.theory_base_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
       | NONE => hint)
     end
   else
@@ -820,9 +820,9 @@
 fun crude_thm_ord ctxt =
   let
     val ancestor_lengths =
-      fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy)))
+      fold (fn thy => Symtab.update (Context.theory_base_name thy, length (Context.ancestors_of thy)))
         (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty
-    val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name
+    val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name {long = false}
 
     fun crude_theory_ord p =
       if Context.eq_thy_id p then EQUAL
@@ -832,9 +832,9 @@
         (case apply2 ancestor_length p of
           (SOME m, SOME n) =>
             (case int_ord (m, n) of
-              EQUAL => string_ord (apply2 Context.theory_id_name p)
+              EQUAL => string_ord (apply2 (Context.theory_id_name {long = false}) p)
             | ord => ord)
-        | _ => string_ord (apply2 Context.theory_id_name p))
+        | _ => string_ord (apply2 (Context.theory_id_name {long = false}) p))
   in
     fn p =>
       (case crude_theory_ord (apply2 Thm.theory_id p) of
@@ -1125,7 +1125,7 @@
             val chunks = app_hd (cons th) chunks
             val chunks_and_parents' =
               if thm_less_eq (th, th') andalso
-                Thm.theory_name th = Thm.theory_name th'
+                Thm.theory_base_name th = Thm.theory_base_name th'
               then (chunks, [nickname_of_thm th])
               else chunks_and_parents_for chunks th'
           in
@@ -1172,11 +1172,11 @@
 
     val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
 
-    fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th
+    fun fact_has_right_theory (_, th) = thy_name = Thm.theory_base_name th
 
     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
       [Thm.prop_of th]
-      |> features_of ctxt (Thm.theory_name th) stature
+      |> features_of ctxt (Thm.theory_base_name th) stature
       |> map (rpair (weight * factor))
   in
     (case get_state ctxt of
@@ -1283,7 +1283,7 @@
     launch_thread timeout (fn () =>
       let
         val thy = Proof_Context.theory_of ctxt
-        val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t]
+        val feats = features_of ctxt (Context.theory_base_name thy) (Local, General) [t]
       in
         map_state ctxt
           (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
@@ -1395,7 +1395,7 @@
                   (learns, (num_nontrivial, next_commit, _)) =
                 let
                   val name = nickname_of_thm th
-                  val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+                  val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
                   val deps = these (deps_of status th)
                   val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
                   val learns = (name, parents, feats, deps) :: learns
@@ -1544,7 +1544,7 @@
     [("", [])]
   else
     let
-      val thy_name = Context.theory_name (Proof_Context.theory_of ctxt)
+      val thy_name = Context.theory_base_name (Proof_Context.theory_of ctxt)
 
       fun maybe_launch_thread exact min_num_facts_to_learn =
         if not (Async_Manager_Legacy.has_running_threads MaShN) andalso
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -220,7 +220,7 @@
     t
 
 fun theory_const_prop_of fudge th =
-  theory_constify fudge (Thm.theory_name th) (Thm.prop_of th)
+  theory_constify fudge (Thm.theory_base_name th) (Thm.prop_of th)
 
 fun pair_consts_fact thy fudge fact =
   (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
@@ -546,7 +546,7 @@
        []
      else
        relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
-         (concl_t |> theory_constify fudge (Context.theory_name thy)))
+         (concl_t |> theory_constify fudge (Context.theory_base_name thy)))
     |> map fact_of_lazy_fact
   end
 
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/sat.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -216,7 +216,7 @@
       handle TERM _ => NONE;  (* 'chyp' is not a literal *)
 
     fun prove_clause id =
-      (case Array.sub (clauses, id) of
+      (case Array.nth clauses id of
         RAW_CLAUSE clause => clause
       | ORIG_CLAUSE thm =>
           (* convert the original clause *)
@@ -226,7 +226,7 @@
             val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
               Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
             val clause = (raw, hyps)
-            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+            val _ = Array.upd clauses id (RAW_CLAUSE clause)
           in
             clause
           end
@@ -236,7 +236,7 @@
             val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
             val ids = the (Inttab.lookup clause_table id)
             val clause = resolve_raw_clauses ctxt (map prove_clause ids)
-            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+            val _ = Array.upd clauses id (RAW_CLAUSE clause)
             val _ =
               cond_tracing ctxt
                 (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
@@ -358,7 +358,7 @@
             val max_idx = fst (the (Inttab.max clause_table))
             val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
             val _ =
-              fold (fn thm => fn i => (Array.update (clause_arr, i, ORIG_CLAUSE thm); i + 1))
+              fold (fn thm => fn i => (Array.upd clause_arr i (ORIG_CLAUSE thm); i + 1))
                 cnf_clauses 0
             (* replay the proof to derive the empty clause *)
             (* [c_1 && ... && c_n] |- False *)
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/sat_solver.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -667,7 +667,7 @@
       fun init_array (Prop_Logic.And (fm1, fm2), n) =
         init_array (fm2, init_array (fm1, n))
         | init_array (fm, n) =
-        (Array.update (clauses, n, clause_to_lit_list fm); n+1)
+        (Array.upd clauses n (clause_to_lit_list fm); n+1)
       val _ = init_array (cnf, 0)
       (* optimization for the common case where MiniSat "R"s clauses in their *)
       (* original order:                                                      *)
@@ -682,7 +682,7 @@
             original_clause_id_from 0
           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
           (* testing for equality should suffice -- barring duplicate literals     *)
-          else if Array.sub (clauses, index) = lits then (
+          else if Array.nth clauses index = lits then (
             (* success *)
             last_ref_clause := index;
             SOME index
diff -r 89676df5846a -r 9c5e8460df05 src/HOL/ex/Join_Theory.thy
--- a/src/HOL/ex/Join_Theory.thy	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/ex/Join_Theory.thy	Sat Apr 22 10:22:41 2023 +0200
@@ -35,7 +35,7 @@
 setup \<open>
   fn thy =>
     let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10)
-    in Theory.join_theory forked_thys end
+    in Context.join_thys forked_thys end
 \<close>
 
 term test1
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/General/array.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/array.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -0,0 +1,33 @@
+(*  Title:      Pure/General/array.ML
+    Author:     Makarius
+
+Additional operations for structure Array, following Isabelle/ML conventions.
+*)
+
+signature ARRAY =
+sig
+  include ARRAY
+  val nth: 'a array -> int -> 'a
+  val upd: 'a array -> int -> 'a -> unit
+  val forall: ('a -> bool) -> 'a array -> bool
+  val member: ('a * 'a -> bool) -> 'a array -> 'a -> bool
+  val fold: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+  val fold_rev: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+end;
+
+structure Array: ARRAY =
+struct
+
+open Array;
+
+fun nth arr i = sub (arr, i);
+fun upd arr i x = update (arr, i, x);
+
+val forall = all;
+
+fun member eq arr x = exists (fn y => eq (x, y)) arr;
+
+fun fold f arr x = foldl (fn (a, b) => f a b) x arr;
+fun fold_rev f arr x = foldr (fn (a, b) => f a b) x arr;
+
+end;
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/General/sha1.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -101,12 +101,12 @@
     (*hash result -- 5 words*)
     val hash_array : Word32.word Array.array =
       Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
-    fun hash i = Array.sub (hash_array, i);
-    fun add_hash x i = Array.update (hash_array, i, hash i + x);
+    val hash = Array.nth hash_array;
+    fun add_hash x i = Array.upd hash_array i (hash i + x);
 
     (*current chunk -- 80 words*)
     val chunk_array = Array.array (80, 0w0: Word32.word);
-    fun chunk i = Array.sub (chunk_array, i);
+    val chunk = Array.nth chunk_array;
     fun init_chunk pos =
       Array.modifyi (fn (i, _) =>
         if i < 16 then text (pos + i)
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/locale.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -355,8 +355,9 @@
     unique registration serial points to mixin list*)
   type T = reg Idtab.table * mixins;
   val empty: T = (Idtab.empty, Inttab.empty);
-  fun merge old_thys =
+  fun merge args =
     let
+      val ctxt0 = Syntax.init_pretty_global (#1 (hd args));
       fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
         (Idtab.merge eq_reg (regs1, regs2), merge_mixins (mixins1, mixins2))
         handle Idtab.DUP id =>
@@ -373,9 +374,9 @@
             val _ =
               warning ("Removed duplicate interpretation after retrieving its mixins" ^
                 Position.here_list [#pos reg1, #pos reg2] ^ ":\n  " ^
-                Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id));
+                Pretty.string_of (pretty_reg_inst ctxt0 [] id));
           in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end;
-    in recursive_merge end;
+    in Library.foldl1 recursive_merge (map #2 args) end;
 );
 
 structure Local_Registrations = Proof_Data
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/named_target.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -97,7 +97,7 @@
        theory_registration = Generic_Target.theory_registration,
        locale_dependency = fn _ => error "Not possible in theory target",
        pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
-        Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+        Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]}
   | operations (Locale locale) =
       {define = Generic_Target.define (locale_foundation locale),
        notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -112,7 +112,7 @@
 (* maintain commands *)
 
 fun add_command name cmd thy =
-  if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
+  if member (op =) Thy_Header.bootstrap_thys (Context.theory_base_name thy) then thy
   else
     let
       val _ =
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -10,7 +10,7 @@
 sig
   val theory_of: Proof.context -> theory
   val init_global: theory -> Proof.context
-  val get_global: theory -> string -> Proof.context
+  val get_global: {long: bool} -> theory -> string -> Proof.context
   type mode
   val mode_default: mode
   val mode_pattern: mode
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/toplevel.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -162,7 +162,7 @@
     Toplevel =>
       (case previous_theory_of state of
         NONE => "at top level"
-      | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
+      | SOME thy => "at top level, result theory " ^ quote (Context.theory_base_name thy))
   | Theory (Context.Theory _) => "in theory mode"
   | Theory (Context.Proof _) => "in local theory mode"
   | Proof _ => "in proof mode"
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -65,7 +65,7 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
     (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
       (Theory.check {long = false} ctxt (name, pos);
-       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+       "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>
 
   ML_Antiquotation.inline \<^binding>\<open>context\<close>
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/ROOT.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -21,6 +21,7 @@
 ML_file "General/basics.ML";
 ML_file "General/string.ML";
 ML_file "General/vector.ML";
+ML_file "General/array.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Syntax/parser.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -132,16 +132,16 @@
       if not new_chain then ([], lambdas)
       else
         let (*lookahead of chain's source*)
-          val ((_, from_tks), _) = Array.sub (prods, the chain);
+          val ((_, from_tks), _) = Array.nth prods (the chain);
 
           (*copy from's lookahead to chain's destinations*)
           fun copy_lookahead to =
             let
-              val ((to_nts, to_tks), ps) = Array.sub (prods, to);
+              val ((to_nts, to_tks), ps) = Array.nth prods to;
 
               val new_tks = Tokens.subtract to_tks from_tks;  (*added lookahead tokens*)
               val to_tks' = Tokens.merge (to_tks, new_tks);
-              val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
+              val _ = Array.upd prods to ((to_nts, to_tks'), ps);
             in tokens_add (to, new_tks) end;
 
           val tos = chains_all_succs chains' [lhs];
@@ -170,7 +170,7 @@
           else (NONE, nts_insert nt nts);
 
     (*get all known starting tokens for a nonterminal*)
-    fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
+    fun starts_for_nt nt = snd (fst (Array.nth prods nt));
 
     (*update prods, lookaheads, and lambdas according to new lambda NTs*)
     val (added_starts', lambdas') =
@@ -180,7 +180,7 @@
           | propagate_lambda (l :: ls) added_starts lambdas =
               let
                 (*get lookahead for lambda NT*)
-                val ((dependent, l_starts), _) = Array.sub (prods, l);
+                val ((dependent, l_starts), _) = Array.nth prods l;
 
                 (*check productions whose lookahead may depend on lambda NT*)
                 fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods =
@@ -221,7 +221,7 @@
                 (*check each NT whose lookahead depends on new lambda NT*)
                 fun process_nts nt (added_lambdas, added_starts) =
                   let
-                    val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+                    val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
 
                     (*existing productions whose lookahead may depend on l*)
                     val tk_prods = prods_lookup nt_prods (get_start l_starts);
@@ -235,7 +235,7 @@
                     val new_tks = Tokens.merge (old_tks, added_tks);
 
                     val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
-                    val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods'));
+                    val _ = Array.upd prods nt ((new_nts, new_tks), nt_prods');
                       (*N.B. that because the tks component
                         is used to access existing
                         productions we have to add new
@@ -279,9 +279,9 @@
           (*add lhs NT to list of dependent NTs in lookahead*)
           fun add_nts nt initial =
             (if initial then
-              let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+              let val ((old_nts, old_tks), ps) = Array.nth prods nt in
                 if nts_member old_nts lhs then ()
-                else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
+                else Array.upd prods nt ((nts_insert lhs old_nts, old_tks), ps)
               end
              else (); false);
 
@@ -290,7 +290,7 @@
           fun add_tks [] added = added
             | add_tks (nt :: nts) added =
                 let
-                  val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+                  val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
 
                   val new_tks = Tokens.subtract old_tks start_tks;
 
@@ -306,9 +306,7 @@
                     |> nt = lhs ? Tokens.fold store start_tks';
                   val _ =
                     if not changed andalso Tokens.is_empty new_tks then ()
-                    else
-                      Array.update
-                        (prods, nt, ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'));
+                    else Array.upd prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods');
                 in add_tks nts (tokens_add (nt, new_tks) added) end;
           val _ = nts_fold add_nts start_nts true;
         in add_tks (chains_all_succs chains' [lhs]) [] end;
@@ -365,7 +363,7 @@
                 (*copy existing productions for new starting tokens*)
                 fun process_nts nt =
                   let
-                    val ((nts, tks), nt_prods) = Array.sub (prods, nt);
+                    val ((nts, tks), nt_prods) = Array.nth prods nt;
 
                     val tk_prods = prods_lookup nt_prods key;
 
@@ -379,10 +377,10 @@
 
                     val added_tks = Tokens.subtract tks new_tks;
                     val tks' = Tokens.merge (tks, added_tks);
-                    val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
+                    val _ = Array.upd prods nt ((nts, tks'), nt_prods'');
                   in tokens_add (nt, added_tks) end;
 
-                val ((dependent, _), _) = Array.sub (prods, changed_nt);
+                val ((dependent, _), _) = Array.nth prods changed_nt;
               in add_starts (starts @ nts_fold process_nts dependent []) end;
       in add_starts added_starts' end;
   in (chains', lambdas') end;
@@ -574,7 +572,7 @@
   filter
     (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
       | _ => false)
-    (Array.sub (Estate, j));
+    (Array.nth Estate j);
 
 
 fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
@@ -652,7 +650,7 @@
 
 
 fun produce gram stateset i indata prev_token =
-  (case Array.sub (stateset, i) of
+  (case Array.nth stateset i of
     [] =>
       let
         val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
@@ -677,8 +675,8 @@
       | c :: cs =>
           let
             val (si, sii) = PROCESSS gram stateset i c s;
-            val _ = Array.update (stateset, i, si);
-            val _ = Array.update (stateset, i + 1, sii);
+            val _ = Array.upd stateset i si;
+            val _ = Array.upd stateset (i + 1) sii;
           in produce gram stateset (i + 1) cs c end));
 
 
@@ -693,7 +691,7 @@
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
-    val _ = Array.update (Estate, 0, S0);
+    val _ = Array.upd Estate 0 S0;
   in
     get_trees (produce gram Estate 0 indata Lexicon.eof)
   end;
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Thy/export_theory.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -414,7 +414,7 @@
         get_dependencies parents thy |> map_index (fn (i, dep) =>
           let
             val xname = string_of_int (i + 1);
-            val name = Long_Name.implode [Context.theory_name thy, xname];
+            val name = Long_Name.implode [Context.theory_base_name thy, xname];
             val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
             val body = encode_locale_dependency dep;
           in XML.Elem (markup, body) end)
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -65,7 +65,7 @@
     else
       let
         val keywords = Thy_Header.get_keywords thy;
-        val thy_name = Context.theory_name thy;
+        val thy_name = Context.theory_base_name thy;
         val latex = Document_Output.present_thy options keywords thy_name segments;
       in
         if Options.string options "document" = "false" then ()
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/named_theorems.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -59,7 +59,7 @@
 
 fun clear name = map_entry name (K Thm.item_net);
 
-fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
+fun add_thm name = map_entry name o Item_Net.update o Thm.trim_context;
 fun del_thm name = map_entry name o Item_Net.remove;
 
 val add = Thm.declaration_attribute o add_thm;
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/named_thms.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Tools/named_thms.ML
     Author:     Makarius
 
-Named collections of theorems in canonical order.
+Named collections of theorems in canonical (reverse) order: OLD VERSION.
 *)
 
 signature NAMED_THMS =
@@ -27,10 +27,10 @@
 
 val member = Item_Net.member o Data.get o Context.Proof;
 
-val content = Item_Net.content o Data.get;
+fun content context = map (Thm.transfer'' context) (Item_Net.content (Data.get context));
 val get = content o Context.Proof;
 
-val add_thm = Data.map o Item_Net.update;
+val add_thm = Data.map o Item_Net.update o Thm.trim_context;
 val del_thm = Data.map o Item_Net.remove;
 
 val add = Thm.declaration_attribute add_thm;
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/thy_deps.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -27,8 +27,8 @@
         SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
       | NONE => K true);
     fun node thy =
-      ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
-        map Context.theory_name (filter pred (Theory.parents_of thy)));
+      ((Context.theory_base_name thy, Graph_Display.content_node (Context.theory_base_name thy) []),
+        map Context.theory_base_name (filter pred (Theory.parents_of thy)));
   in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
 
 val thy_deps =
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/axclass.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -74,6 +74,8 @@
       (*constant name ~> type constructor ~> (constant name, equation)*)
     (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)};
 
+fun rep_data (Data args) = args;
+
 fun make_data (axclasses, params, inst_params) =
   Data {axclasses = axclasses, params = params, inst_params = inst_params};
 
@@ -81,22 +83,23 @@
 (
   type T = data;
   val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty));
-  fun merge old_thys
-      (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1},
-       Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) =
+  fun merge args =
     let
-      val old_ctxt = Syntax.init_pretty_global (fst old_thys);
+      val ctxt0 = Syntax.init_pretty_global (#1 (hd args));
 
-      val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
-      val params' =
+      fun merge_params (params1, params2) =
         if null params1 then params2
         else
-          fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
+          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt0 p)
             params2 params1;
 
-      val inst_params' =
+      fun merge_inst_params (inst_params1, inst_params2) =
         (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
           Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
+
+      val axclasses' = Library.foldl1 (Symtab.merge (K true)) (map (#axclasses o rep_data o #2) args);
+      val params' = Library.foldl1 merge_params (map (#params o rep_data o #2) args);
+      val inst_params' = Library.foldl1 merge_inst_params (map (#inst_params o rep_data o #2) args);
     in make_data (axclasses', params', inst_params') end;
 );
 
@@ -116,11 +119,11 @@
   map_data (fn (axclasses, params, inst_params) =>
     (axclasses, params, f inst_params));
 
-val rep_data = Data.get #> (fn Data args => args);
+val rep_theory_data = Data.get #> rep_data;
 
-val axclasses_of = #axclasses o rep_data;
-val params_of = #params o rep_data;
-val inst_params_of = #inst_params o rep_data;
+val axclasses_of = #axclasses o rep_theory_data;
+val params_of = #params o rep_theory_data;
+val inst_params_of = #inst_params o rep_theory_data;
 
 
 (* axclasses with parameters *)
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/context.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -20,26 +20,29 @@
   sig
     val theory_of: Proof.context -> theory
     val init_global: theory -> Proof.context
-    val get_global: theory -> string -> Proof.context
+    val get_global: {long: bool} -> theory -> string -> Proof.context
   end
 end;
 
 signature CONTEXT =
 sig
   include BASIC_CONTEXT
+  (*theory data*)
+  type data_kind = int
+  val data_kinds: unit -> (data_kind * Position.T) list
   (*theory context*)
+  type id = int
   type theory_id
   val theory_id: theory -> theory_id
   val timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_ord: theory_id ord
-  val theory_id_long_name: theory_id -> string
-  val theory_id_name: theory_id -> string
+  val theory_id_name: {long: bool} -> theory_id -> string
   val theory_long_name: theory -> string
-  val theory_name: theory -> string
-  val theory_name': {long: bool} -> theory -> string
-  val theory_identifier: theory -> serial
+  val theory_base_name: theory -> string
+  val theory_name: {long: bool} -> theory -> string
+  val theory_identifier: theory -> id
   val PureN: string
   val pretty_thy: theory -> Pretty.T
   val pretty_abbrev_thy: theory -> Pretty.T
@@ -52,7 +55,7 @@
   val subthy: theory * theory -> bool
   val trace_theories: bool Unsynchronized.ref
   val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int}
-  val join_thys: theory * theory -> theory
+  val join_thys: theory list -> theory
   val begin_thy: string -> theory list -> theory
   val finish_thy: theory -> theory
   val theory_data_sizeof1: theory -> (Position.T * int) list
@@ -96,15 +99,15 @@
   include CONTEXT
   structure Theory_Data:
   sig
-    val declare: Position.T -> Any.T -> (theory * theory -> Any.T * Any.T -> Any.T) -> serial
-    val get: serial -> (Any.T -> 'a) -> theory -> 'a
-    val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
+    val declare: Position.T -> Any.T -> ((theory * Any.T) list -> Any.T) -> data_kind
+    val get: data_kind -> (Any.T -> 'a) -> theory -> 'a
+    val put: data_kind -> ('a -> Any.T) -> 'a -> theory -> theory
   end
   structure Proof_Data:
   sig
-    val declare: (theory -> Any.T) -> serial
-    val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
-    val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
+    val declare: (theory -> Any.T) -> data_kind
+    val get: data_kind -> (Any.T -> 'a) -> Proof.context -> 'a
+    val put: data_kind -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
   end
 end;
 
@@ -113,24 +116,39 @@
 
 (*** theory context ***)
 
+(* theory data *)
+
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
+type data_kind = int;
+val data_kind = Counter.make ();
+
 
 (** datatype theory **)
 
-type stage = int * int Synchronized.var;
-fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1);
-fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state);
+(* implicit state *)
+
+type state = {stage: int} Synchronized.var;
+
+fun make_state () : state =
+  Synchronized.var "Context.state" {stage = 0};
+
+fun next_stage (state: state) =
+  Synchronized.change_result state (fn {stage} => (stage + 1, {stage = stage + 1}));
+
+
+(* theory_id *)
+
+type id = int;
+val new_id = Counter.make ();
 
 abstype theory_id =
   Theory_Id of
-   (*identity*)
-   {id: serial,                   (*identifier*)
-    ids: Intset.T} *              (*cumulative identifiers -- symbolic body content*)
-   (*history*)
-   {name: string,                 (*official theory name*)
-    stage: stage option}          (*index and counter for anonymous updates*)
+   {id: id,                       (*identifier*)
+    ids: Intset.T,                (*cumulative identifiers -- symbolic body content*)
+    name: string,                 (*official theory name*)
+    stage: int}                   (*index for anonymous updates*)
 with
 
 fun rep_theory_id (Theory_Id args) = args;
@@ -138,8 +156,13 @@
 
 end;
 
+
+(* theory *)
+
 datatype theory =
   Theory of
+   (*allocation state*)
+   state *
    (*identity*)
    {theory_id: theory_id,
     token: Position.T Unsynchronized.ref} *
@@ -153,26 +176,28 @@
 
 fun rep_theory (Theory args) = args;
 
-val theory_identity = #1 o rep_theory;
+val state_of = #1 o rep_theory;
+val theory_identity = #2 o rep_theory;
 val theory_id = #theory_id o theory_identity;
-val identity_of_id = #1 o rep_theory_id;
-val identity_of = identity_of_id o theory_id;
-val history_of_id = #2 o rep_theory_id;
-val history_of = history_of_id o theory_id;
-val ancestry_of = #2 o rep_theory;
-val data_of = #3 o rep_theory;
+val identity_of = rep_theory_id o theory_id;
+val ancestry_of = #3 o rep_theory;
+val data_of = #4 o rep_theory;
 
-fun make_identity id ids = {id = id, ids = ids};
-fun make_history name = {name = name, stage = SOME (init_stage ())};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
-val theory_id_ord = int_ord o apply2 (#id o identity_of_id);
-val theory_id_long_name = #name o history_of_id;
-val theory_id_name = Long_Name.base_name o theory_id_long_name;
-val theory_long_name = #name o history_of;
-val theory_name = Long_Name.base_name o theory_long_name;
-fun theory_name' {long} = if long then theory_long_name else theory_name;
-val theory_identifier = #id o identity_of_id o theory_id;
+fun stage_final stage = stage = 0;
+
+val theory_id_stage = #stage o rep_theory_id;
+val theory_id_final = stage_final o theory_id_stage;
+val theory_id_ord = int_ord o apply2 (#id o rep_theory_id);
+fun theory_id_name {long} thy_id =
+  let val name = #name (rep_theory_id thy_id)
+  in if long then name else Long_Name.base_name name end;
+
+val theory_long_name = #name o identity_of;
+val theory_base_name = Long_Name.base_name o theory_long_name;
+fun theory_name {long} = if long then theory_long_name else theory_base_name;
+val theory_identifier = #id o identity_of;
 
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;
@@ -183,9 +208,10 @@
 val PureN = "Pure";
 
 fun display_name thy_id =
-  (case history_of_id thy_id of
-    {name, stage = NONE} => name
-  | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i);
+  let
+    val name = theory_id_name {long = false} thy_id;
+    val final = theory_id_final thy_id;
+  in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end;
 
 fun display_names thy =
   let
@@ -205,31 +231,24 @@
   in Pretty.str_list "{" "}" abbrev end;
 
 fun get_theory long thy name =
-  if theory_name' long thy <> name then
-    (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
+  if theory_name long thy <> name then
+    (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of
       SOME thy' => thy'
     | NONE => error ("Unknown ancestor theory " ^ quote name))
-  else if is_none (#stage (history_of thy)) then thy
+  else if theory_id_final (theory_id thy) then thy
   else error ("Unfinished theory " ^ quote name);
 
 
-(* build ids *)
+(* identity *)
 
-val merge_ids =
-  apply2 (theory_id #> rep_theory_id #> #1) #>
-  (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) =>
-    Intset.merge (ids1, ids2)
-    |> Intset.insert id1
-    |> Intset.insert id2);
+fun merge_ids thys =
+  fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id))
+    thys Intset.empty;
 
-
-(* equality and inclusion *)
-
-val eq_thy_id = op = o apply2 (#id o identity_of_id);
+val eq_thy_id = op = o apply2 (#id o rep_theory_id);
 val eq_thy = op = o apply2 (#id o identity_of);
 
-val proper_subthy_id =
-  apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
+val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
 val proper_subthy = proper_subthy_id o apply2 theory_id;
 
 fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
@@ -240,7 +259,7 @@
 
 fun eq_thy_consistent (thy1, thy2) =
   eq_thy (thy1, thy2) orelse
-    (theory_name thy1 = theory_name thy2 andalso
+    (theory_base_name thy1 = theory_base_name thy2 andalso
       raise THEORY ("Duplicate theory name", [thy1, thy2]));
 
 fun extend_ancestors thy thys =
@@ -250,6 +269,11 @@
 
 val merge_ancestors = merge eq_thy_consistent;
 
+val eq_ancestry =
+  apply2 ancestry_of #>
+    (fn ({parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
+      eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors'));
+
 
 
 (** theory data **)
@@ -263,33 +287,53 @@
 type kind =
  {pos: Position.T,
   empty: Any.T,
-  merge: theory * theory -> Any.T * Any.T -> Any.T};
+  merge: (theory * Any.T) list -> Any.T};
 
 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
 
-fun invoke name f k x =
+fun the_kind k =
   (case Datatab.lookup (Synchronized.value kinds) k of
-    SOME kind =>
-      if ! timing andalso name <> "" then
-        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
-          (fn () => f kind x)
-      else f kind x
+    SOME kind => kind
   | NONE => raise Fail "Invalid theory data identifier");
 
 in
 
-fun invoke_pos k = invoke "" (K o #pos) k ();
-fun invoke_empty k = invoke "" (K o #empty) k ();
-fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+fun data_kinds () =
+  Datatab.fold_rev (fn (k, {pos, ...}) => cons (k, pos)) (Synchronized.value kinds) [];
+
+val invoke_pos = #pos o the_kind;
+val invoke_empty = #empty o the_kind;
 
-fun declare_theory_data pos empty merge =
+fun invoke_merge kind args =
+  if ! timing then
+    Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind))
+      (fn () => #merge kind args)
+  else #merge kind args;
+
+fun declare_data pos empty merge =
   let
-    val k = serial ();
+    val k = data_kind ();
     val kind = {pos = pos, empty = empty, merge = merge};
     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   in k end;
 
-fun merge_data thys = Datatab.join (invoke_merge thys);
+fun lookup_data k thy = Datatab.lookup (data_of thy) k;
+
+fun get_data k thy =
+  (case lookup_data k thy of
+    SOME x => x
+  | NONE => invoke_empty k);
+
+fun merge_data [] = Datatab.empty
+  | merge_data [thy] = data_of thy
+  | merge_data thys =
+      let
+        fun merge (k, kind) data =
+          (case map_filter (fn thy => lookup_data k thy |> Option.map (pair thy)) thys of
+            [] => data
+          | [(_, x)] => Datatab.default (k, x) data
+          | args => Datatab.update (k, invoke_merge kind args) data);
+      in Datatab.fold merge (Synchronized.value kinds) (data_of (hd thys)) end;
 
 end;
 
@@ -331,11 +375,11 @@
      total = length trace}
   end;
 
-fun create_thy ids history ancestry data =
+fun create_thy state ids name stage ancestry data =
   let
-    val theory_id = make_theory_id (make_identity (serial ()) ids, history);
-    val token = make_token ();
-  in Theory ({theory_id = theory_id, token = token}, ancestry, data) end;
+    val theory_id = make_theory_id {id = new_id (), ids = ids, name = name, stage = stage};
+    val identity = {theory_id = theory_id, token = make_token ()};
+  in Theory (state, identity, ancestry, data) end;
 
 end;
 
@@ -343,102 +387,80 @@
 (* primitives *)
 
 val pre_pure_thy =
-  create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
+  let
+    val state = make_state ();
+    val stage = next_stage state;
+  in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end;
 
 local
 
 fun change_thy finish f thy =
   let
-    val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy);
-    val Theory (_, ancestry, data) = thy;
+    val {name, stage, ...} = identity_of thy;
+    val Theory (state, _, ancestry, data) = thy;
     val ancestry' =
-      if is_none stage
+      if stage_final stage
       then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
       else ancestry;
-    val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
-    val ids' = Intset.insert id ids;
+    val ids' = merge_ids [thy];
+    val stage' = if finish then 0 else next_stage state;
     val data' = f data;
-  in create_thy ids' history' ancestry' data' end;
+  in create_thy state ids' name stage' ancestry' data' end;
 
 in
 
 val update_thy = change_thy false;
-val extend_thy = change_thy false I;
 val finish_thy = change_thy true I;
 
 end;
 
 
-(* join: anonymous theory nodes *)
-
-local
-
-fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]);
+(* join: unfinished theory nodes *)
 
-fun join_history thys =
-  apply2 history_of thys |>
-  (fn ({name, stage}, {name = name', stage = stage'}) =>
-    if name = name' andalso is_some stage andalso is_some stage' then
-      {name = name, stage = Option.map next_stage stage}
-    else bad_join thys);
+fun join_thys [] = raise List.Empty
+  | join_thys thys =
+      let
+        val thy0 = hd thys;
+        val name0 = theory_long_name thy0;
+        val state0 = state_of thy0;
 
-fun join_ancestry thys =
-  apply2 ancestry_of thys |>
-  (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
-    if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')
-    then ancestry else bad_join thys);
-
-in
+        fun ok thy =
+          not (theory_id_final (theory_id thy)) andalso
+          theory_long_name thy = name0 andalso
+          eq_ancestry (thy0, thy);
+        val _ =
+          (case filter_out ok thys of
+            [] => ()
+          | bad => raise THEORY ("Cannot join theories", bad));
 
-fun join_thys thys =
-  let
-    val ids = merge_ids thys;
-    val history = join_history thys;
-    val ancestry = join_ancestry thys;
-    val data = merge_data thys (apply2 data_of thys);
-  in create_thy ids history ancestry data end;
-
-end;
+        val stage = next_stage state0;
+        val ids = merge_ids thys;
+        val data = merge_data thys;
+      in create_thy state0 ids name0 stage (ancestry_of thy0) data end;
 
 
-(* merge: named theory nodes *)
-
-local
+(* merge: finished theory nodes *)
 
-fun merge_thys thys =
-  let
-    val ids = merge_ids thys;
-    val history = make_history "";
-    val ancestry = make_ancestry [] [];
-    val data = merge_data thys (apply2 data_of thys);
-  in create_thy ids history ancestry data end;
-
-fun maximal_thys thys =
-  thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
-
-in
+fun make_parents thys =
+  let val thys' = distinct eq_thy thys
+  in thys' |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys') end;
 
 fun begin_thy name imports =
   if name = "" then error ("Bad theory name: " ^ quote name)
+  else if null imports then error "Missing theory imports"
   else
     let
-      val parents = maximal_thys (distinct eq_thy imports);
+      val parents = make_parents imports;
       val ancestors =
-        Library.foldl merge_ancestors ([], map ancestors_of parents)
+        Library.foldl1 merge_ancestors (map ancestors_of parents)
         |> fold extend_ancestors parents;
+      val ancestry = make_ancestry parents ancestors;
 
-      val thy0 =
-        (case parents of
-          [] => error "Missing theory imports"
-        | [thy] => extend_thy thy
-        | thy :: thys => Library.foldl merge_thys (thy, thys));
-      val ({ids, ...}, _) = rep_theory_id (theory_id thy0);
-
-      val history = make_history name;
-      val ancestry = make_ancestry parents ancestors;
-    in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
-
-end;
+      val state = make_state ();
+      val stage = next_stage state;
+      val ids = merge_ids parents;
+      val data = merge_data parents;
+    in create_thy state ids name stage ancestry data |> tap finish_thy end;
 
 
 (* theory data *)
@@ -446,14 +468,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;
@@ -509,7 +528,7 @@
 struct
   fun theory_of (Proof.Context (_, thy)) = thy;
   fun init_global thy = Proof.Context (init_data thy, thy);
-  fun get_global thy name = init_global (get_theory {long = false} thy name);
+  fun get_global long thy name = init_global (get_theory long thy name);
 end;
 
 structure Proof_Data =
@@ -517,7 +536,7 @@
 
 fun declare init =
   let
-    val k = serial ();
+    val k = data_kind ();
     val _ = Synchronized.change kinds (Datatab.update (k, init));
   in k end;
 
@@ -526,8 +545,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;
 
@@ -633,7 +652,7 @@
 sig
   type T
   val empty: T
-  val merge: theory * theory -> T * T -> T
+  val merge: (theory * T) list -> T
 end;
 
 signature THEORY_DATA_ARGS =
@@ -662,7 +681,7 @@
     Context.Theory_Data.declare
       pos
       (Data Data.empty)
-      (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)))
+      (Data o Data.merge o map (fn (thy, Data x) => (thy, x)))
   end;
 
 val get = Context.Theory_Data.get kind (fn Data x => x);
@@ -676,7 +695,7 @@
   (
     type T = Data.T;
     val empty = Data.empty;
-    fun merge _ = Data.merge;
+    fun merge args = Library.foldl (fn (a, (_, b)) => Data.merge (a, b)) (#2 (hd args), tl args)
   );
 
 
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/cterm_items.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -19,6 +19,8 @@
 
 end;
 
+structure Ctermset = Set(Ctermtab.Key);
+
 
 structure Cterms:
 sig
@@ -54,3 +56,5 @@
 fun thm_cache f = Cache.create empty lookup update f;
 
 end;
+
+structure Thmset = Set(Thmtab.Key);
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/global_theory.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -172,9 +172,9 @@
   let
     val theories =
       Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
-        Symtab.update (Context.theory_name thy', thy')));
+        Symtab.update (Context.theory_long_name thy', thy')));
     fun transfer th =
-      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
+      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_long_name th))) th;
   in transfer end;
 
 fun all_thms_of thy verbose =
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/morphism.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -22,6 +22,7 @@
     typ: (typ -> typ) list,
     term: (term -> term) list,
     fact: (thm list -> thm list) list} -> morphism
+  val is_identity: morphism -> bool
   val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
   val binding_prefix: morphism -> (string * bool) list
@@ -82,6 +83,10 @@
     term = map (pair a) term,
     fact = map (pair a) fact};
 
+(*syntactic test only!*)
+fun is_identity (Morphism {names, binding, typ, term, fact}) =
+  null names andalso null binding andalso null typ andalso null term andalso null fact;
+
 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/proofterm.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -2137,7 +2137,7 @@
 fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
 
 fun export_proof_boxes_required thy =
-  Context.theory_name thy = Context.PureN orelse
+  Context.theory_long_name thy = Context.PureN orelse
     (export_enabled () andalso not (export_standard_enabled ()));
 
 fun export_proof_boxes bodies =
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/sign.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -129,24 +129,23 @@
   tsig: Type.tsig,              (*order-sorted signature of types*)
   consts: Consts.T};            (*polymorphic constants*)
 
+fun rep_sign (Sign args) = args;
 fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
 
 structure Data = Theory_Data'
 (
   type T = sign;
   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
-  fun merge old_thys (sign1, sign2) =
+  fun merge args =
     let
-      val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
-      val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
-
-      val syn = Syntax.merge_syntax (syn1, syn2);
-      val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
-      val consts = Consts.merge (consts1, consts2);
-    in make_sign (syn, tsig, consts) end;
+      val context0 = Context.Theory (#1 (hd args));
+      val syn' = Library.foldl1 Syntax.merge_syntax (map (#syn o rep_sign o #2) args);
+      val tsig' = Library.foldl1 (Type.merge_tsig context0) (map (#tsig o rep_sign o #2) args);
+      val consts' = Library.foldl1 Consts.merge (map (#consts o rep_sign o #2) args);
+    in make_sign (syn', tsig', consts') end;
 );
 
-fun rep_sg thy = Data.get thy |> (fn Sign args => args);
+val rep_sg = rep_sign o Data.get;
 
 fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
 
@@ -514,7 +513,7 @@
 val mandatory_path = map_naming o Name_Space.mandatory_path;
 val qualified_path = map_naming oo Name_Space.qualified_path;
 
-fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy);
 
 fun init_naming thy =
   let
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/theory.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -22,7 +22,6 @@
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
   val at_end: (theory -> theory option) -> theory -> theory
-  val join_theory: theory list -> theory
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
@@ -83,6 +82,8 @@
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
+fun rep_thy (Thy args) = args;
+
 fun make_thy (pos, id, axioms, defs, wrappers) =
   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
 
@@ -90,19 +91,22 @@
 (
   type T = thy;
   val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
-  fun merge old_thys (thy1, thy2) =
+  fun merge args =
     let
-      val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
-      val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
+      val thy0 = #1 (hd args);
+      val {pos, id, ...} = rep_thy (#2 (hd args));
 
-      val axioms' = Name_Space.merge_tables (axioms1, axioms2);
-      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
-      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
-      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
+      val merge_defs = Defs.merge (Defs.global_context thy0);
+      val merge_wrappers = Library.merge (eq_snd op =);
+
+      val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args);
+      val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args);
+      val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args);
+      val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args);
     in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
 );
 
-fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
+val rep_theory = rep_thy o Thy.get;
 
 fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   make_thy (f (pos, id, axioms, defs, wrappers)));
@@ -143,7 +147,7 @@
             val completion_report =
               Completion.make_report (name, pos)
                 (fn completed =>
-                  map (Context.theory_name' long) (ancestors_of thy)
+                  map (Context.theory_name long) (ancestors_of thy)
                   |> filter (completed o Long_Name.base_name)
                   |> sort_strings
                   |> map (fn a => (a, (Markup.theoryN, a))));
@@ -162,13 +166,6 @@
 val defs_of = #defs o rep_theory;
 
 
-(* join theory *)
-
-fun join_theory [] = raise List.Empty
-  | join_theory [thy] = thy
-  | join_theory thys = foldl1 Context.join_thys thys;
-
-
 (* begin/end theory *)
 
 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
diff -r 89676df5846a -r 9c5e8460df05 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/thm.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -66,7 +66,9 @@
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_id: thm -> Context.theory_id
-  val theory_name: thm -> string
+  val theory_name: {long: bool} -> thm -> string
+  val theory_long_name: thm -> string
+  val theory_base_name: thm -> string
   val maxidx_of: thm -> int
   val maxidx_thm: thm -> int -> int
   val shyps_of: thm -> sort Ord_List.T
@@ -177,7 +179,7 @@
   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
-  val thynames_of_arity: theory -> string * class -> string list
+  val theory_names_of_arity: {long: bool} -> theory -> string * class -> string list
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
 end;
@@ -494,7 +496,10 @@
 
 val cert_of = #cert o rep_thm;
 val theory_id = Context.certificate_theory_id o cert_of;
-val theory_name = Context.theory_id_name o theory_id;
+
+fun theory_name long = Context.theory_id_name long o theory_id;
+val theory_long_name = theory_name {long = true};
+val theory_base_name = theory_name {long = false};
 
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
@@ -2338,10 +2343,10 @@
 
 (* type arities *)
 
-fun thynames_of_arity thy (a, c) =
+fun theory_names_of_arity {long} thy (a, c) =
   build (get_arities thy |> Aritytab.fold
     (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
-  |> sort (int_ord o apply2 #2) |> map #1;
+  |> sort (int_ord o apply2 #2) |> map (if long then #1 else Long_Name.base_name o #1);
 
 fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
   let
@@ -2399,7 +2404,7 @@
     val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
     val prop = plain_prop_of th;
     val (t, Ss, c) = Logic.dest_arity prop;
-    val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ()));
+    val ar = ((t, Ss, c), (th', Context.theory_long_name thy, serial ()));
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
diff -r 89676df5846a -r 9c5e8460df05 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_runtime.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -718,7 +718,7 @@
         val code_binding = Path.map_binding Code_Target.code_path binding;
         val preamble =
           "(* Generated from " ^
-            Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
+            Path.implode (Resources.thy_path (Path.basic (Context.theory_base_name thy))) ^
           "; DO NOT EDIT! *)";
         val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
         val _ = Code_Target.code_export_message thy';
diff -r 89676df5846a -r 9c5e8460df05 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_symbol.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -99,7 +99,7 @@
 local
   val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space;
   val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space;
-  fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
+  fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst
    of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
     | thyname :: _ => thyname;
   fun thyname_of_const thy c = case Axclass.class_of_param thy c
diff -r 89676df5846a -r 9c5e8460df05 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML	Sat Apr 22 10:22:41 2023 +0200
@@ -1009,7 +1009,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     fun this_theory name =
-      if Context.theory_name thy = name then thy
+      if Context.theory_base_name thy = name then thy
       else Context.get_theory {long = false} thy name;
 
     fun consts_of thy' =