# HG changeset patch
# User paulson
# Date 1721424572 -3600
# Node ID ffef122946a301cd28f3d933cd891d09e9ebd98d
# Parent  839c4f8742f9ddfc86fec339f885f87e6f5ec970# Parent  f2eb4fa955250aaadb209a032acdca56b68a279a
merged

diff -r f2eb4fa95525 -r ffef122946a3 NEWS
--- a/NEWS	Fri Jul 19 22:29:16 2024 +0100
+++ b/NEWS	Fri Jul 19 22:29:32 2024 +0100
@@ -32,6 +32,9 @@
       wfP_trancl ~> wfp_tranclp
       wfP_wf_eq ~> wfp_wf_eq
       wf_acc_iff ~> wf_iff_acc
+  - Added lemmas.
+      wf_on_antimono_stronger
+      wfp_on_antimono_stronger
 
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
diff -r f2eb4fa95525 -r ffef122946a3 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Doc/Implementation/Logic.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -1293,7 +1293,7 @@
   @{define_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{define_ML Proofterm.expand_proof: "theory ->
-  (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
+  (Proofterm.thm_header -> Thm_Name.P option) -> proof -> proof"} \\
   @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
   @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -67,13 +67,13 @@
    GT \<Rightarrow> let r' = insert x r in if incr r r' then balR l a b r' else Node l (a,b) r')"
 
 fun decr where
-"decr t t' = (t \<noteq> Leaf \<and> (t' = Leaf \<or> \<not> is_bal t \<and> is_bal t'))"
+"decr t t' = (t \<noteq> Leaf \<and> incr t' t)"
 
 fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal * 'a" where
 "split_max (Node l (a, ba) r) =
   (if r = Leaf then (l,a)
    else let (r',a') = split_max r;
-            t' = if decr r r' then balL l a ba r' else Node l (a,ba) r'
+            t' = if incr r' r then balL l a ba r' else Node l (a,ba) r'
         in (t', a'))"
 
 fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
@@ -82,7 +82,7 @@
   (case cmp x a of
      EQ \<Rightarrow> if l = Leaf then r
            else let (l', a') = split_max l in
-                if decr l l' then balR l' a' ba r else Node l' (a',ba) r |
+                if incr l' l then balR l' a' ba r else Node l' (a',ba) r |
      LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
      GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
 
@@ -136,7 +136,7 @@
 
 lemma avl_split_max:
   "\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-   avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
+   avl t' \<and> height t = height t' + (if incr t' t then 1 else 0)"
 apply(induction t arbitrary: t' a rule: split_max_induct)
  apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
 done
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -307,10 +307,13 @@
 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
 by (induction t) auto
 
+lemma bheight_le_min_height:  "invh t \<Longrightarrow> bheight t \<le> min_height t"
+by (induction t) auto
+
 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
 proof -
   have "2 powr (height t / 2) \<le> 2 powr bheight t"
-    using rbt_height_bheight[OF assms] by (simp)
+    using rbt_height_bheight[OF assms] by simp
   also have "\<dots> \<le> size1 t" using assms
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
@@ -319,4 +322,15 @@
   thus ?thesis by simp
 qed
 
+lemma rbt_height_le2: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
+proof -
+  have "height t \<le> 2 * bheight t"
+    using rbt_height_bheight_if assms[simplified rbt_def] by fastforce
+  also have "\<dots> \<le> 2 * min_height t"
+    using bheight_le_min_height assms[simplified rbt_def] by auto
+  also have "\<dots> \<le> 2 * log 2 (size1 t)"
+    using le_log2_of_power min_height_size1 by auto
+  finally show ?thesis by simp
+qed
+
 end
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -14,11 +14,11 @@
 ML \<open>
   fun export_proof thy thm = thm
     |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
-    |> Proofterm.encode (Sign.consts_of thy);
+    |> Proofterm.encode thy;
 
   fun import_proof thy xml =
     let
-      val prf = Proofterm.decode (Sign.consts_of thy) xml;
+      val prf = Proofterm.decode thy xml;
       val (prf', _) = Proofterm.freeze_thaw_prf prf;
     in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
 \<close>
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -16,7 +16,7 @@
 fun thm_name_of thm =
   (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
       [Thm.proof_of thm] [] of
-    [thm_name] => thm_name
+    [(thm_name, _)] => thm_name
   | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
 
 val short_name_of = Thm_Name.short o thm_name_of;
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -305,9 +305,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = (("HOL.cong", 0), _), ...}, _) % _ % _ % SOME x % SOME y %%
       prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
-  | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
+  | strip_cong ps (PThm ({thm_name = (("HOL.refl", 0), _), ...}, _) % SOME f %% _) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
 val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
   | elim_cong_aux _ _ = NONE;
diff -r f2eb4fa95525 -r ffef122946a3 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -309,18 +309,45 @@
 
 subsubsection \<open>Antimonotonicity\<close>
 
+
+lemma wfp_on_antimono_stronger:
+  fixes
+    A :: "'a set" and B :: "'b set" and
+    f :: "'a \<Rightarrow> 'b" and
+    R :: "'b \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  assumes
+    wf: "wfp_on B R" and
+    sub: "f ` A \<subseteq> B" and
+    mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R (f x) (f y)"
+  shows "wfp_on A Q"
+  unfolding wfp_on_iff_ex_minimal
+proof (intro allI impI)
+  fix A' :: "'a set"
+  assume "A' \<subseteq> A" and "A' \<noteq> {}"
+  have "f ` A' \<subseteq> B"
+    using \<open>A' \<subseteq> A\<close> sub by blast
+  moreover have "f ` A' \<noteq> {}"
+    using \<open>A' \<noteq> {}\<close> by blast
+  ultimately have "\<exists>z\<in>f ` A'. \<forall>y. R y z \<longrightarrow> y \<notin> f ` A'"
+    using wf wfp_on_iff_ex_minimal by blast
+  hence "\<exists>z\<in>A'. \<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> A'"
+    by blast
+  thus "\<exists>z\<in>A'. \<forall>y. Q y z \<longrightarrow> y \<notin> A'"
+    using \<open>A' \<subseteq> A\<close> mono by blast
+qed
+
+lemma wf_on_antimono_stronger:
+  assumes
+    "wf_on B r" and
+    "f ` A \<subseteq> B" and
+    "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (f x, f y) \<in> r)"
+  shows "wf_on A q"
+  using assms wfp_on_antimono_stronger[to_set, of B r f A q] by blast
+
 lemma wf_on_antimono_strong:
   assumes "wf_on B r" and "A \<subseteq> B" and "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (x, y) \<in> r)"
   shows "wf_on A q"
-  unfolding wf_on_iff_ex_minimal
-proof (intro allI impI)
-  fix AA assume "AA \<subseteq> A" and "AA \<noteq> {}"
-  hence "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> AA"
-    using \<open>wf_on B r\<close> \<open>A \<subseteq> B\<close>
-    by (simp add: wf_on_iff_ex_minimal)
-  then show "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> q \<longrightarrow> y \<notin> AA"
-    using \<open>AA \<subseteq> A\<close> assms(3) by blast
-qed
+  using assms wf_on_antimono_stronger[of B r "\<lambda>x. x" A q] by blast
 
 lemma wfp_on_antimono_strong:
   "wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> wfp_on A Q"
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Build/build_manager.scala	Fri Jul 19 22:29:32 2024 +0100
@@ -980,8 +980,7 @@
   /* repository poller */
 
   object Poller {
-    case class Versions(isabelle: String, components: List[Component])
-    case class State(current: Versions, next: Future[Versions])
+    case class State(current: List[Component], next: Future[List[Component]])
   }
 
   class Poller(
@@ -994,11 +993,11 @@
 
     override def delay = options.seconds("build_manager_poll_delay")
 
-    private def current: Poller.Versions =
-      Poller.Versions(isabelle_repository.id("default"), sync_dirs.map(dir =>
-        Component(dir.name, dir.hg.id("default"))))
+    private def current: List[Component] =
+      Component.isabelle(isabelle_repository.id("default")) ::
+        sync_dirs.map(dir => Component(dir.name, dir.hg.id("default")))
 
-    private def poll: Future[Poller.Versions] = Future.fork {
+    private def poll: Future[List[Component]] = Future.fork {
       Par_List.map((repo: Mercurial.Repository) => repo.pull(),
         isabelle_repository :: sync_dirs.map(_.hg))
 
@@ -1007,17 +1006,24 @@
 
     val init: Poller.State = Poller.State(current, poll)
 
-    private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = {
-      val isabelle_updated = current.isabelle != next.isabelle
-      val updated_components =
-        next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet
+    private def add_tasks(current: List[Component], next: List[Component]): Unit = {
+      val next_rev = next.map(component => component.name -> component.rev).toMap
+
+      def is_unchanged(components: List[Component]): Boolean =
+        components.forall(component => next_rev.get(component.name).contains(component.rev))
+
+      def is_changed(component_names: List[String]): Boolean =
+        !is_unchanged(current.filter(component => component_names.contains(component.name)))
+
+      def is_current(job: Job): Boolean = is_unchanged(job.components)
 
       synchronized_database("add_tasks") {
         for {
           ci_job <- ci_jobs
           if ci_job.trigger == Build_CI.On_Commit
-          if isabelle_updated || ci_job.components.exists(updated_components.contains)
+          if is_changed(Component.Isabelle :: ci_job.components)
           if !_state.pending.values.exists(_.kind == ci_job.name)
+          if !_state.running.values.filter(_.kind == ci_job.name).exists(is_current)
         } _state = _state.add_pending(CI_Build.task(ci_job))
       }
     }
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -283,8 +283,8 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
-      if #serial header = #serial thm_id then Thm_Name.empty
-      else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
+      if #serial header = #serial thm_id then Thm_Name.none
+      else the_default Thm_Name.none (lookup_thm_id (Proofterm.thm_header_id header));
 
     fun entity_markup_thm (serial, (name, i)) =
       let
@@ -310,11 +310,11 @@
         (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;
-            val encode_proof = Proofterm.encode_standard_proof consts;
+            val encode_proof = Proofterm.encode_standard_proof thy;
           in triple encode_prop (list Thm_Name.encode) encode_proof end
       end;
 
-    fun export_thm (thm_id, thm_name) =
+    fun export_thm (thm_id, (thm_name, _)) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val body =
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/General/table.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -66,7 +66,8 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -591,12 +592,13 @@
 
 (* cache *)
 
+type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+
 fun unsynchronized_cache f =
   let
     val cache1 = Unsynchronized.ref empty;
     val cache2 = Unsynchronized.ref empty;
-  in
-    fn x =>
+    fun apply x =
       (case lookup (! cache1) x of
         SOME y => y
       | NONE =>
@@ -604,9 +606,11 @@
             SOME exn => Exn.reraise exn
           | NONE =>
               (case Exn.result f x of
-                Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
-              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
-  end;
+                Exn.Res y => (Unsynchronized.change cache1 (default (x, y)); y)
+              | Exn.Exn exn => (Unsynchronized.change cache2 (default (x, exn)); Exn.reraise exn))));
+    fun reset () = (cache2 := empty; cache1 := empty);
+    fun total_size () = size (! cache1) + size (! cache2);
+  in {apply = apply, reset = reset, size = total_size} end;
 
 
 (* ML pretty-printing *)
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -511,9 +511,9 @@
     val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc [];
-    fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+    fun expand_name ({thm_name = (thm_name, _), ...}: Proofterm.thm_header) =
       if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
-      then SOME Thm_Name.empty else NONE;
+      then SOME Thm_Name.none else NONE;
     val prep = the_default (K I) prep thy' o
       Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
       Proofterm.expand_proof thy' expand_name;
@@ -623,7 +623,7 @@
 
       | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
           let
-            val {pos, theory_name, thm_name, prop, ...} = thm_header;
+            val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -650,8 +650,8 @@
                     val corr_prf = mkabsp shyps corr_prf0;
                     val corr_prop = Proofterm.prop_of corr_prf;
                     val corr_header =
-                      Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name thm_name vs', 0) corr_prop
+                      Proofterm.thm_header (serial ()) command_pos theory_name
+                        ((corr_name thm_name vs', 0), thm_pos) corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf' =
                       Proofterm.proof_combP
@@ -727,7 +727,7 @@
 
       | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
           let
-            val {pos, theory_name, thm_name, prop, ...} = thm_header;
+            val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -772,8 +772,8 @@
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Proofterm.prop_of corr_prf';
                     val corr_header =
-                      Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name thm_name vs', 0) corr_prop
+                      Proofterm.thm_header (serial ()) command_pos theory_name
+                        ((corr_name thm_name vs', 0), thm_pos) corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -88,7 +88,7 @@
               (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
-        fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
+        fun thm_of _ _ (PThm ({thm_name = (thm_name, thm_pos), prop = prop', types = SOME Ts, ...}, _)) =
               let
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name));
                 val prop = Thm.prop_of thm;
@@ -96,9 +96,9 @@
                   if is_equal prop prop' then ()
                   else
                     error ("Duplicate use of theorem name " ^
-                      quote (Global_Theory.print_thm_name thy thm_name) ^ "\n" ^
-                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
-                      Syntax.string_of_term_global thy prop');
+                      quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
+                      ^ "\n" ^ Syntax.string_of_term_global thy prop
+                      ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
               in thm_of_atom thm Ts end
 
           | thm_of _ _ (PAxm (name, _, SOME Ts)) =
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -39,12 +39,12 @@
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
 
-    fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
-        (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
-      | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
-        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
-        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm ({thm_name = (("Pure.protectD", 0), _), ...}, _) % _ %%
+        (PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _) % _ %% prf)) = SOME prf
+      | rew' (PThm ({thm_name = (("Pure.conjunctionD1", 0), _), ...}, _) % _ % _ %%
+        (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm ({thm_name = (("Pure.conjunctionD2", 0), _), ...}, _) % _ % _ %%
+        (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -54,14 +54,14 @@
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
@@ -245,7 +245,7 @@
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+        (PThm ({thm_name = (thm_name, _), prop, types = SOME Ts, ...}, _), ts) =>
           if member (op =) defs thm_name then
             let
               val vs = vars_of prop;
@@ -271,11 +271,11 @@
         let
           val cnames = map (fst o dest_Const o fst) defs';
           val expand = Proofterm.fold_proof_atoms true
-            (fn PThm ({serial, thm_name, prop, ...}, _) =>
+            (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) =>
                 if member (op =) defnames thm_name orelse
                   not (exists_Const (member (op =) cnames o #1) prop)
                 then I
-                else Inttab.update (serial, Thm_Name.empty)
+                else Inttab.update (serial, Thm_Name.none)
               | _ => I) [prf] Inttab.empty;
         in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -16,7 +16,7 @@
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_proof_boxes_of: Proof.context ->
     {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
-  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
+  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.P option} ->
     thm -> Proofterm.proof
   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -104,7 +104,7 @@
   let val U = Term.itselfT T --> propT
   in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
-fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = (a, _), types = Ts, ...}, _)) =
       fold AppT (these Ts)
         (Const
           (Long_Name.append "thm"
@@ -227,7 +227,7 @@
 fun proof_syntax prf =
   let
     val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
-      (fn PThm ({thm_name, ...}, _) =>
+      (fn PThm ({thm_name = (thm_name, _), ...}, _) =>
           if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name)
         | _ => I) [prf] Symset.empty);
     val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
@@ -264,7 +264,7 @@
        excluded = is_some o Global_Theory.lookup_thm_id thy}
   in
     Proofterm.proof_boxes selection [Thm.proof_of thm]
-    |> map (fn ({serial = i, pos, prop, ...}, proof) =>
+    |> map (fn ({serial = i, command_pos, prop, thm_name = (_, thm_pos), ...}, proof) =>
         let
           val proof' = proof
             |> Proofterm.reconstruct_proof thy prop
@@ -276,7 +276,7 @@
           val name = Long_Name.append "thm" (string_of_int i);
         in
           Pretty.item
-           [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
+           [Pretty.str (name ^ Position.here_list [command_pos, thm_pos] ^ ":"), Pretty.brk 1,
             Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
         end)
     |> Pretty.chunks
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/global_theory.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -13,13 +13,13 @@
   val defined_fact: theory -> string -> bool
   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
-  val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+  val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list
   val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
   val print_thm_name: theory -> Thm_Name.T -> string
-  val get_thm_names: theory -> Thm_Name.T Inttab.table
-  val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
-  val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
-  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
+  val get_thm_names: theory -> Thm_Name.P Inttab.table
+  val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list
+  val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option
+  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.P) option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
@@ -63,7 +63,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * Thm_Name.T Inttab.table lazy option;
+  type T = Facts.T * Thm_Name.P Inttab.table lazy option;
   val empty: T = (Facts.empty, NONE);
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
 );
@@ -86,7 +86,7 @@
 
 fun dest_thms verbose prev_thys thy =
   Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
-  |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms |> map (apfst fst));
+  |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
 
 fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
 val print_thm_name = Pretty.string_of oo pretty_thm_name;
@@ -99,7 +99,7 @@
 
 fun make_thm_names thy =
   (dest_thms true (Theory.parents_of thy) thy, Inttab.empty)
-  |-> fold (fn (thm_name, thm) => fn thm_names =>
+  |-> fold (fn ((thm_name, thm_pos), thm) => fn thm_names =>
     (case Thm.derivation_id (Thm.transfer thy thm) of
       NONE => thm_names
     | SOME {serial, theory_name} =>
@@ -107,11 +107,11 @@
           raise THM ("Bad theory name for derivation", 0, [thm])
         else
           (case Inttab.lookup thm_names serial of
-            SOME thm_name' =>
+            SOME (thm_name', thm_pos') =>
               raise THM ("Duplicate use of derivation identity for " ^
-                print_thm_name thy thm_name ^ " vs. " ^
-                print_thm_name thy thm_name', 0, [thm])
-          | NONE => Inttab.update (serial, thm_name) thm_names)));
+                print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^
+                print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm])
+          | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names)));
 
 fun lazy_thm_names thy =
   (case thm_names_of thy of
@@ -256,7 +256,7 @@
       No_Name_Flags => thm
     | Name_Flags {post, official} =>
         thm
-        |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
+        |> (official andalso (post orelse Thm_Name.is_empty (#1 (Thm.raw_derivation_name thm)))) ?
             Thm.name_derivation (name, pos)
         |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/proofterm.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -9,7 +9,7 @@
 signature PROOFTERM =
 sig
   type thm_header =
-    {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+    {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
       prop: term, types: typ list option}
   type thm_body
   type thm_node
@@ -38,7 +38,7 @@
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
-  val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
+  val thm_header: serial -> Position.T -> string -> Thm_Name.P -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
@@ -65,12 +65,13 @@
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
 
-  val encode: Consts.T -> proof XML.Encode.T
-  val encode_body: Consts.T -> proof_body XML.Encode.T
-  val encode_standard_term: Consts.T -> term XML.Encode.T
-  val encode_standard_proof: Consts.T -> proof XML.Encode.T
-  val decode: Consts.T -> proof XML.Decode.T
-  val decode_body: Consts.T -> proof_body XML.Decode.T
+  val proof_to_zproof: theory -> proof -> zproof
+  val encode_standard_term: theory -> term XML.Encode.T
+  val encode_standard_proof: theory -> proof XML.Encode.T
+  val encode: theory -> proof XML.Encode.T
+  val encode_body: theory -> proof_body XML.Encode.T
+  val decode: theory -> proof XML.Decode.T
+  val decode_body: theory -> proof_body XML.Decode.T
 
   val %> : proof * term -> proof
 
@@ -170,8 +171,8 @@
   val reconstruct_proof: theory -> term -> proof -> proof
   val prop_of': term list -> proof -> term
   val prop_of: proof -> term
-  val expand_name_empty: thm_header -> Thm_Name.T option
-  val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
+  val expand_name_empty: thm_header -> Thm_Name.P option
+  val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
 
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
@@ -188,8 +189,8 @@
   val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
     term -> (serial * proof_body future) list -> proof_body -> term * proof_body
   val get_identity: sort list -> term list -> term -> proof ->
-    {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
-  val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
+    {serial: serial, theory_name: string, thm_name: Thm_Name.P} option
+  val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.P
   type thm_id = {serial: serial, theory_name: string}
   val make_thm_id: serial * string -> thm_id
   val thm_header_id: thm_header -> thm_id
@@ -205,8 +206,10 @@
 
 (** datatype proof **)
 
+val proof_serial = Counter.make ();
+
 type thm_header =
-  {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+  {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
     prop: term, types: typ list option};
 
 datatype proof =
@@ -253,8 +256,8 @@
 fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
   PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
 
-fun thm_header serial pos theory_name thm_name prop types : thm_header =
-  {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name,
+fun thm_header serial command_pos theory_name thm_name prop types : thm_header =
+  {serial = serial, command_pos = command_pos, theory_name = theory_name, thm_name = thm_name,
     prop = prop, types = types};
 
 fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
@@ -290,7 +293,9 @@
 
 val no_export = Lazy.value ();
 
-fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+fun make_thm
+    ({serial, theory_name, thm_name = (thm_name, _), prop, ...}: thm_header)
+    (Thm_Body {body, ...}) =
   (serial, make_thm_node theory_name thm_name prop body no_export);
 
 
@@ -342,8 +347,8 @@
   | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
   | no_thm_names (prf % t) = no_thm_names prf % t
   | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
-  | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) =
-      PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body)
+  | no_thm_names (PThm ({serial, command_pos, theory_name, thm_name = _, prop, types}, thm_body)) =
+      PThm (thm_header serial command_pos theory_name Thm_Name.none prop types, thm_body)
   | no_thm_names a = a;
 
 fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -369,6 +374,39 @@
 
 (** XML data representation **)
 
+(* encode as zterm/zproof *)
+
+fun proof_to_zproof thy =
+  let
+    val {ztyp, zterm} = ZTerm.zterm_cache thy;
+    val ztvar = ztyp #> (fn ZTVar v => v);
+
+    fun zproof_const name prop typargs =
+      let
+        val vs = rev ((fold_types o fold_atyps) (insert (op =) o ztvar) prop []);
+        val Ts = map ztyp typargs
+      in ZConstp ((name, zterm prop), (ZTVars.make (vs ~~ Ts), ZVars.empty)) end;
+
+    fun zproof MinProof = ZNop
+      | zproof (PBound i) = ZBoundp i
+      | zproof (Abst (a, SOME T, p)) = ZAbst (a, ztyp T, zproof p)
+      | zproof (AbsP (a, SOME t, p)) = ZAbsp (a, zterm t, zproof p)
+      | zproof (p % SOME t) = ZAppt (zproof p, zterm t)
+      | zproof (p %% q) = ZAppp (zproof p, zproof q)
+      | zproof (Hyp t) = ZHyp (zterm t)
+      | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
+      | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
+      | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
+      | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+          let val proof_name =
+            ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
+          in zproof_const proof_name prop Ts end;
+  in zproof end;
+
+fun encode_standard_term thy = ZTerm.zterm_of thy #> ZTerm.encode_zterm {typed_vars = false};
+fun encode_standard_proof thy = proof_to_zproof thy #> ZTerm.encode_zproof {typed_vars = false};
+
+
 (* encode *)
 
 local
@@ -386,11 +424,13 @@
   fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn PClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
-  fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
-    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)],
-      pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
-        (map Position.properties_of pos,
-          (prop, (types, map_proof_of open_proof (Future.join body)))))]
+  fn PThm ({serial, command_pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+      ([int_atom serial, theory_name],
+        pair (properties o Position.properties_of)
+          (pair Thm_Name.encode_pos
+            (pair (term consts)
+              (pair (option (list typ)) (proof_body consts))))
+        (command_pos, (thm_name, (prop, (types, map_proof_of open_proof (Future.join body))))))]
 and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) =
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
@@ -399,39 +439,10 @@
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
-fun standard_term consts t = t |> variant
- [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, _) => ([a], []),
-  fn Var (a, _) => (indexname a, []),
-  fn Bound a => ([], int a),
-  fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
-  fn t as op $ a =>
-    if can Logic.match_of_class t then raise Match
-    else ([], pair (standard_term consts) (standard_term consts) a),
-  fn t =>
-    let val (T, c) = Logic.match_of_class t
-    in ([c], typ T) end];
-
-fun standard_proof consts prf = prf |> variant
- [fn MinProof => ([], []),
-  fn PBound a => ([], int a),
-  fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
-  fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
-  fn Hyp a => ([], standard_term consts a),
-  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
-  fn PClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
-  fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
-    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
-
 in
 
-val encode = proof;
-val encode_body = proof_body;
-val encode_standard_term = standard_term;
-val encode_standard_proof = standard_proof;
+val encode = proof o Sign.consts_of;
+val encode_body = proof_body o Sign.consts_of;
 
 end;
 
@@ -453,12 +464,14 @@
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
   fn ([b], a) => PClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
-  fn ([a, b, c, d], e) =>
+  fn ([ser, theory_name], b) =>
     let
-      val ((x, (y, (z, w)))) =
-        pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e;
-      val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z;
-    in PThm (header, thm_body w) end]
+      val ((command_pos, (thm_name, (prop, (types, body))))) =
+        pair (Position.of_properties o properties)
+          (pair Thm_Name.decode_pos
+            (pair (term consts) (pair (option (list typ)) (proof_body consts)))) b;
+      val header = thm_header (int_atom ser) command_pos theory_name thm_name prop types;
+    in PThm (header, thm_body body) end]
 and proof_body consts x =
   let
     val (a, b, c) =
@@ -473,8 +486,8 @@
 
 in
 
-val decode = proof;
-val decode_body = proof_body;
+val decode = proof o Sign.consts_of;
+val decode_body = proof_body o Sign.consts_of;
 
 end;
 
@@ -562,8 +575,8 @@
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
       | proof (PClass C) = ofclass C
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
-      | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
-          PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
+      | proof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
+          PThm (thm_header serial command_pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
@@ -603,8 +616,8 @@
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
-  | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) =
-      PThm (thm_header serial pos theory_name thm_name prop types, thm_body)
+  | change_types types (PThm ({serial, command_pos, theory_name, thm_name, prop, types = _}, thm_body)) =
+      PThm (thm_header serial command_pos theory_name thm_name prop types, thm_body)
   | change_types _ prf = prf;
 
 
@@ -768,7 +781,7 @@
           PClass (norm_type_same T, c)
       | norm (Oracle (a, prop, Ts)) =
           Oracle (a, prop, Same.map_option norm_types_same Ts)
-      | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
+      | norm (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
           PThm (thm_header i p theory_name thm_name t
             (Same.map_option norm_types_same Ts), thm_body)
       | norm _ = raise Same.SAME;
@@ -1029,8 +1042,8 @@
       | proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
       | proof _ _ (PClass (T, c)) = PClass (typ T, c)
       | proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
-      | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) =
-          PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body)
+      | proof _ _ (PThm ({serial, command_pos, theory_name, thm_name, prop, types}, thm_body)) =
+          PThm (thm_header serial command_pos theory_name thm_name prop (typs types), thm_body)
       | proof _ _ _ = raise Same.SAME;
 
     val k = length prems;
@@ -1452,7 +1465,7 @@
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
       | subst _ _ (PClass (T, c)) = PClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) =
+      | subst _ _ (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop, types}, thm_body)) =
           PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body)
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1627,7 +1640,7 @@
   | guess_name (prf %% PClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf
   | guess_name (prf % SOME (Var _)) = guess_name prf
-  | guess_name _ = Thm_Name.empty;
+  | guess_name _ = Thm_Name.none;
 
 
 (* generate constraints for proof term *)
@@ -1739,7 +1752,8 @@
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (prop_types ~~ Ts)
               (forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
-                error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf)))
+                error ("Wrong number of type arguments for " ^
+                  quote (Thm_Name.print_pos (guess_name prf)))
           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1927,7 +1941,7 @@
 (* expand and reconstruct subproofs *)
 
 fun expand_name_empty (header: thm_header) =
-  if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
+  if Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE;
 
 fun expand_proof thy expand_name prf =
   let
@@ -1946,10 +1960,10 @@
           let val (seen', maxidx', prf') = expand seen maxidx prf
           in (seen', maxidx', prf' % t) end
       | expand seen maxidx (prf as PThm (header, thm_body)) =
-          let val {serial, pos, theory_name, thm_name, prop, types} = header in
+          let val {serial, command_pos, theory_name, thm_name, prop, types} = header in
             (case expand_name header of
               SOME thm_name' =>
-                if #1 thm_name' = "" andalso is_some types then
+                if #1 (#1 thm_name') = "" andalso is_some types then
                   let
                     val (seen', maxidx', prf') =
                       (case Inttab.lookup seen serial of
@@ -1968,7 +1982,7 @@
                   in (seen', maxidx' + maxidx + 1, prf'') end
                 else if thm_name' <> thm_name then
                   (seen, maxidx,
-                    PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
+                    PThm (thm_header serial command_pos theory_name thm_name' prop types, thm_body))
                 else (seen, maxidx, prf)
             | NONE => (seen, maxidx, prf))
           end
@@ -2160,13 +2174,12 @@
     val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
     val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
 
-    val consts = Sign.consts_of thy;
     val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
       let
         open XML.Encode Term_XML.Encode;
         val encode_vars = list (pair string typ);
-        val encode_term = encode_standard_term consts;
-        val encode_proof = encode_standard_proof consts;
+        val encode_term = encode_standard_term thy;
+        val encode_proof = encode_standard_proof thy;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
   in
     Export.export_params (Context.Theory thy)
@@ -2199,7 +2212,7 @@
 
     fun new_prf () =
       let
-        val i = serial ();
+        val i = proof_serial ();
         val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
         val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
         val body1 =
@@ -2211,11 +2224,11 @@
       if export_enabled () then new_prf ()
       else
         (case strip_combt (proof_head_of proof0) of
-          (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+          (PThm ({serial = ser, thm_name = (a, _), prop = prop', types = NONE, ...}, thm_body'), args') =>
             if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
               let
                 val Thm_Body {body = body', ...} = thm_body';
-                val i = if #1 a = "" andalso named then serial () else ser;
+                val i = if #1 a = "" andalso named then proof_serial () else ser;
               in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
             else new_prf ()
         | _ => new_prf ());
@@ -2244,7 +2257,7 @@
     val theory_name = Context.theory_long_name thy;
     val thm = (i, make_thm_node theory_name name prop1 thm_body export);
 
-    val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
+    val header = thm_header i (Position.thread_data ()) theory_name (name, pos) prop1 NONE;
     val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
     val argst =
       if unconstrain then
@@ -2283,7 +2296,7 @@
   end;
 
 fun get_approximative_name shyps hyps prop prf =
-  Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
+  Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.none;
 
 
 (* thm_id *)
@@ -2302,7 +2315,7 @@
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
-  | SOME {serial, theory_name, thm_name, ...} =>
+  | SOME {serial, theory_name, thm_name = (thm_name, _), ...} =>
       if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name)));
 
 fun this_id NONE _ = false
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_items.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -34,7 +34,8 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -86,6 +87,7 @@
 fun make2 e1 e2 = build (add e1 #> add e2);
 fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
 
+type 'a cache_ops = 'a Table.cache_ops;
 val unsynchronized_cache = Table.unsynchronized_cache;
 
 
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_xml.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -12,7 +12,6 @@
   val sort: sort T
   val typ: typ T
   val term_raw: term T
-  val typ_body: typ T
   val term: Consts.T -> term T
 end
 
@@ -47,12 +46,12 @@
   fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
   fn op $ a => ([], pair term_raw term_raw a)];
 
-fun typ_body T = if T = dummyT then [] else typ T;
+fun var_type T = if T = dummyT then [] else typ T;
 
 fun term consts t = t |> variant
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, b) => ([a], typ_body b),
-  fn Var (a, b) => (indexname a, typ_body b),
+  fn Free (a, b) => ([a], var_type b),
+  fn Var (a, b) => (indexname a, var_type b),
   fn Bound a => ([], int a),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn t as op $ a =>
@@ -87,13 +86,13 @@
   fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair term_raw term_raw a)];
 
-fun typ_body [] = dummyT
-  | typ_body body = typ body;
+fun var_type [] = dummyT
+  | var_type body = typ body;
 
 fun term consts body = body |> variant
  [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
-  fn ([a], b) => Free (a, typ_body b),
-  fn (a, b) => Var (indexname a, typ_body b),
+  fn ([a], b) => Free (a, var_type b),
+  fn (a, b) => Var (indexname a, var_type b),
   fn ([], a) => Bound (int a),
   fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair (term consts) (term consts) a),
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_xml.scala	Fri Jul 19 22:29:32 2024 +0100
@@ -25,13 +25,13 @@
         { case TFree(a, b) => (List(a), sort(b)) },
         { case TVar(a, b) => (indexname(a), sort(b)) }))
 
-    val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
+    private val var_type: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
 
     def term: T[Term] =
       variant[Term](List(
         { case Const(a, b) => (List(a), list(typ)(b)) },
-        { case Free(a, b) => (List(a), typ_body(b)) },
-        { case Var(a, b) => (indexname(a), typ_body(b)) },
+        { case Free(a, b) => (List(a), var_type(b)) },
+        { case Var(a, b) => (indexname(a), var_type(b)) },
         { case Bound(a) => (Nil, int(a)) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) },
@@ -53,13 +53,13 @@
         { case (List(a), b) => TFree(a, sort(b)) },
         { case (a, b) => TVar(indexname(a), sort(b)) }))
 
-    val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
+    private val var_type: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
     def term: T[Term] =
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) },
-        { case (List(a), b) => Free(a, typ_body(b)) },
-        { case (a, b) => Var(indexname(a), typ_body(b)) },
+        { case (List(a), b) => Free(a, var_type(b)) },
+        { case (a, b) => Var(indexname(a), var_type(b)) },
         { case (Nil, a) => Bound(int(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
@@ -72,8 +72,8 @@
       def term: T[Term] =
         variant[Term](List(
           { case (List(a), b) => Const(a, list(typ)(b)) },
-          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
-          { case (a, b) => Var(indexname(a), typ_body(b)) },
+          { case (List(a), b) => Free(a, env_type(a, var_type(b))) },
+          { case (a, b) => Var(indexname(a), var_type(b)) },
           { case (Nil, a) => Bound(int(a)) },
           { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
           { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -120,8 +120,8 @@
   val derivation_closed: thm -> bool
   val derivation_name: thm -> Thm_Name.T
   val derivation_id: thm -> Proofterm.thm_id option
-  val raw_derivation_name: thm -> Thm_Name.T
-  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+  val raw_derivation_name: thm -> Thm_Name.P
+  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option
   val name_derivation: Thm_Name.P -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
@@ -1100,8 +1100,8 @@
                 SOME T' => T'
               | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
         val map_ztyp =
-          ZTypes.unsynchronized_cache
-            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
+          #apply (ZTypes.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;
@@ -1131,13 +1131,13 @@
         NONE => K false
       | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
     fun expand header =
-      if self_id header orelse Thm_Name.is_empty (#thm_name header)
-      then SOME Thm_Name.empty else NONE;
+      if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header))
+      then SOME Thm_Name.none else NONE;
   in expand end;
 
 (*deterministic name of finished proof*)
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
-  Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
+  #1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm));
 
 (*identified PThm node*)
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm_deps.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -59,7 +59,7 @@
       else
         let val thm_id = Proofterm.thm_id (i, thm_node) in
           (case lookup thm_id of
-            SOME thm_name =>
+            SOME (thm_name, _) =>
               Inttab.update (i, SOME (thm_id, thm_name)) res
           | NONE =>
               Inttab.update (i, NONE) res
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm_name.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -26,9 +26,12 @@
   val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
   val print_suffix: T -> string
   val print: T -> string
+  val print_pos: P -> string
   val short: T -> string
   val encode: T XML.Encode.T
   val decode: T XML.Decode.T
+  val encode_pos: P XML.Encode.T
+  val decode_pos: P XML.Decode.T
 end;
 
 structure Thm_Name: THM_NAME =
@@ -106,6 +109,8 @@
 
 fun print (name, index) = name ^ print_suffix (name, index);
 
+fun print_pos (thm_name, pos) = print thm_name ^ Position.here pos;
+
 fun short (name, index) =
   if name = "" orelse index = 0 then name
   else name ^ "_" ^ string_of_int index;
@@ -116,4 +121,7 @@
 val encode = let open XML.Encode in pair string int end;
 val decode = let open XML.Decode in pair string int end;
 
+val encode_pos = let open XML.Encode in pair encode (properties o Position.properties_of) end;
+val decode_pos = let open XML.Decode in pair decode (Position.of_properties o properties) end;
+
 end;
diff -r f2eb4fa95525 -r ffef122946a3 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/zterm.ML	Fri Jul 19 22:29:32 2024 +0100
@@ -251,10 +251,15 @@
   val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
   val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
   val ztyp_of: typ -> ztyp
+  val ztyp_dummy: ztyp
+  val typ_of_tvar: indexname * sort -> typ
+  val typ_of: ztyp -> typ
+  val reset_cache: theory -> theory
+  val check_cache: theory -> {ztyp: int, typ: int} option
+  val ztyp_cache: theory -> typ -> ztyp
+  val typ_cache: theory -> ztyp -> typ
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm
-  val typ_of_tvar: indexname * sort -> typ
-  val typ_of: ztyp -> typ
   val term_of: theory -> zterm -> term
   val beta_norm_term_same: zterm Same.operation
   val beta_norm_proof_same: zproof Same.operation
@@ -262,7 +267,7 @@
   val beta_norm_term: zterm -> zterm
   val beta_norm_proof: zproof -> zproof
   val beta_norm_prooft: zproof -> zproof
-  val norm_type: Type.tyenv -> ztyp -> ztyp
+  val norm_type: theory -> Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
   val zproof_const_typargs: zproof_const -> ((indexname * sort) * ztyp) list
@@ -310,6 +315,9 @@
   val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
     typ * sort -> zproof list
   val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
+  val encode_ztyp: ztyp XML.Encode.T
+  val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
+  val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
 end;
 
 structure ZTerm: ZTERM =
@@ -470,7 +478,7 @@
 
 fun instantiate_type_same instT =
   if ZTVars.is_empty instT then Same.same
-  else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
+  else #apply (ZTypes.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));
@@ -577,7 +585,7 @@
   in Same.commit proof end;
 
 
-(* convert ztyp / zterm vs. regular typ / term *)
+(* convert ztyp vs. regular typ *)
 
 fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
   | ztyp_of (TVar v) = ZTVar v
@@ -587,13 +595,75 @@
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
-fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+val ztyp_dummy = ztyp_of dummyT;
+
+fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
+  | typ_of_tvar v = TVar v;
+
+fun typ_of (ZTVar v) = typ_of_tvar v
+  | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
+  | typ_of ZProp = propT
+  | typ_of (ZType0 c) = Type (c, [])
+  | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
+  | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
+
+
+(* cache within theory context *)
+
+local
+
+structure Data = Theory_Data
+(
+  type T = (ztyp Typtab.cache_ops * typ ZTypes.cache_ops) option;
+  val empty = NONE;
+  val merge = K NONE;
+);
+
+fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
+fun init_cache thy =
+  if is_some (Data.get thy) then NONE
+  else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
+
+fun exit_cache thy =
+  (case Data.get thy of
+    SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
+  | NONE => NONE);
+
+in
+
+val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
+
+fun reset_cache thy =
+  (case Data.get thy of
+    SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); thy)
+  | NONE => thy);
+
+fun check_cache thy =
+  Data.get thy
+  |> Option.map (fn (cache1, cache2) => {ztyp = #size cache1 (), typ = #size cache2 ()});
+
+fun ztyp_cache thy =
+  (case Data.get thy of
+    SOME (cache, _) => cache
+  | NONE => make_ztyp_cache ()) |> #apply;
+
+fun typ_cache thy =
+  (case Data.get thy of
+    SOME (_, cache) => cache
+  | NONE => make_typ_cache ()) |> #apply;
+
+end;
+
+
+(* convert zterm vs. regular term *)
 
 fun zterm_cache thy =
   let
     val typargs = Consts.typargs (Sign.consts_of thy);
 
-    val ztyp = ztyp_cache ();
+    val ztyp = ztyp_cache thy;
 
     fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp T)
       | zterm (Var (xi, T)) = ZVar (xi, ztyp T)
@@ -612,18 +682,6 @@
 
 val zterm_of = #zterm o zterm_cache;
 
-fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
-  | typ_of_tvar v = TVar v;
-
-fun typ_of (ZTVar v) = typ_of_tvar v
-  | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
-  | typ_of ZProp = propT
-  | typ_of (ZType0 c) = Type (c, [])
-  | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
-  | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
-
-fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
-
 fun term_of thy =
   let
     val instance = Consts.instance (Sign.consts_of thy);
@@ -717,11 +775,13 @@
         | norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts);
     in norm end;
 
-fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) =
+fun norm_term_same {ztyp, zterm} (envir as Envir.Envir {tyenv, tenv, ...}) =
   let
     val lookup =
       if Vartab.is_empty tenv then K NONE
-      else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+      else
+        #apply (ZVars.unsynchronized_cache
+          (apsnd typ_of #> Envir.lookup envir #> Option.map zterm));
 
     val normT = norm_type_same ztyp tyenv;
 
@@ -776,15 +836,9 @@
         in beta_norm_prooft (map_proof {hyps = false} inst_typ norm_term prf) end
   end;
 
-fun norm_cache thy =
-  let
-    val {ztyp, zterm} = zterm_cache thy;
-    val typ = typ_cache ();
-  in {ztyp = ztyp, zterm = zterm, typ = typ} end;
-
-fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv);
-fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir);
-fun norm_proof thy envir = norm_proof_cache (norm_cache thy) envir;
+fun norm_type thy tyenv = Same.commit (norm_type_same (ztyp_cache thy) tyenv);
+fun norm_term thy envir = Same.commit (norm_term_same (zterm_cache thy) envir);
+fun norm_proof thy envir = norm_proof_cache (zterm_cache thy) envir;
 
 
 
@@ -870,7 +924,8 @@
     val typ_operation = #typ_operation ucontext {strip_sorts = true};
     val unconstrain_typ = Same.commit typ_operation;
     val unconstrain_ztyp =
-      ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
+      #apply (ZTypes.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);
 
@@ -1087,10 +1142,10 @@
     val typ =
       if Names.is_empty tfrees then Same.same
       else
-        ZTypes.unsynchronized_cache
+        #apply (ZTypes.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)
@@ -1112,10 +1167,10 @@
     let
       val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
       val typ =
-        ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+        #apply (ZTypes.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 =
@@ -1124,7 +1179,7 @@
   | SOME f =>
       let
         val tvar = ztyp_of o Same.function f;
-        val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
+        val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
       in map_proof_types {hyps = false} typ prf end);
 
 
@@ -1158,7 +1213,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 ZTypes.unsynchronized_cache (subst_type_same tvar) end;
+    in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
 
 fun incr_indexes_proof inc prf =
   let
@@ -1240,7 +1295,7 @@
 
 fun assumption_proof thy envir Bs Bi n visible prf =
   let
-    val cache as {zterm, ...} = norm_cache thy;
+    val cache as {zterm, ...} = zterm_cache thy;
     val normt = zterm #> Same.commit (norm_term_same cache envir);
   in
     ZAbsps (map normt Bs)
@@ -1258,7 +1313,7 @@
 
 fun bicompose_proof thy env smax flatten Bs As A oldAs n m visible rprf sprf =
   let
-    val cache as {zterm, ...} = norm_cache thy;
+    val cache as {zterm, ...} = zterm_cache thy;
     val normt = zterm #> Same.commit (norm_term_same cache env);
     val normp = norm_proof_cache cache env visible;
 
@@ -1292,12 +1347,14 @@
 
 fun unconstrainT_proof thy sorts_proof (ucontext: Logic.unconstrain_context) =
   let
-    val cache = norm_cache thy;
     val algebra = Sign.classes_of thy;
 
+    val cache = zterm_cache thy;
+    val typ_cache = typ_cache thy;
+
     val typ =
-      ZTypes.unsynchronized_cache
-        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
+      #apply (ZTypes.unsynchronized_cache
+        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
 
     val typ_sort = #typ_operation ucontext {strip_sorts = false};
 
@@ -1307,11 +1364,67 @@
       | NONE => raise Fail "unconstrainT_proof: missing constraint");
 
     fun class (T, c) =
-      let val T' = Same.commit typ_sort (#typ cache T)
+      let val T' = Same.commit typ_sort (typ_cache T)
       in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end;
   in
     map_proof_types {hyps = false} typ #> map_class_proof class #> beta_norm_prooft
     #> fold_rev (implies_intr_proof' o #zterm cache o #2) (#constraints ucontext)
   end;
 
+
+
+(** XML data representation **)
+
+(* encode *)
+
+local
+
+open XML.Encode Term_XML.Encode;
+
+fun ztyp T = T |> variant
+ [fn ZFun args => (["fun"], pair ztyp ztyp args)
+   | ZProp => (["prop"], [])
+   | ZType0 a => ([a], [])
+   | ZType1 (a, b) => ([a], list ztyp [b])
+   | ZType (a, b) => ([a], list ztyp b),
+  fn ZTVar ((a, ~1), b) => ([a], sort b),
+  fn ZTVar (a, b) => (indexname a, sort b)];
+
+fun zvar_type {typed_vars} T =
+  if typed_vars andalso T <> ztyp_dummy then ztyp T else [];
+
+fun zterm flag t = t |> variant
+ [fn ZConst0 a => ([a], [])
+   | ZConst1 (a, b) => ([a], list ztyp [b])
+   | ZConst (a, b) => ([a], list ztyp b),
+  fn ZVar ((a, ~1), b) => ([a], zvar_type flag b),
+  fn ZVar (a, b) => (indexname a, zvar_type flag b),
+  fn ZBound a => ([], int a),
+  fn ZAbs (a, b, c) => ([a], pair ztyp (zterm flag) (b, c)),
+  fn ZApp a => ([], pair (zterm flag) (zterm flag) a),
+  fn OFCLASS (a, b) => ([b], ztyp a)];
+
+fun zproof flag prf = prf |> variant
+ [fn ZNop => ([], []),
+  fn ZBoundp a => ([], int a),
+  fn ZAbst (a, b, c) => ([a], pair ztyp (zproof flag) (b, c)),
+  fn ZAbsp (a, b, c) => ([a], pair (zterm flag) (zproof flag) (b, c)),
+  fn ZAppt a => ([], pair (zproof flag) (zterm flag) a),
+  fn ZAppp a => ([], pair (zproof flag) (zproof flag) a),
+  fn ZHyp a => ([], zterm flag a),
+  fn ZConstp (c as ((ZAxiom a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn OFCLASSp (a, b) => ([b], ztyp a),
+  fn ZConstp (c as ((ZOracle a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn ZConstp (c as ((ZThm {theory_name, thm_name = (name, _), serial}, b), _)) =>
+    ([int_atom serial, theory_name, #1 name, int_atom (#2 name)],
+      list (ztyp o #2) (zproof_const_typargs c))];
+
+in
+
+val encode_ztyp = ztyp;
+val encode_zterm = zterm;
+val encode_zproof = zproof;
+
 end;
+
+end;
diff -r f2eb4fa95525 -r ffef122946a3 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Fri Jul 19 22:29:32 2024 +0100
@@ -2651,7 +2651,7 @@
 
 {-# LANGUAGE LambdaCase #-}
 
-module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Encode (indexname, sort, typ, term)
 where
 
 import Isabelle.Library
@@ -2671,15 +2671,15 @@
     \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
     \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }]
 
-typ_body :: T Typ
-typ_body ty = if is_dummyT ty then [] else typ ty
+var_type :: T Typ
+var_type ty = if is_dummyT ty then [] else typ ty
 
 term :: T Term
 term t =
   t |> variant
    [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
-    \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing },
-    \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
+    \case { Free (a, b) -> Just ([a], var_type b); _ -> Nothing },
+    \case { Var (a, b) -> Just (indexname a, var_type b); _ -> Nothing },
     \case { Bound a -> Just ([], int a); _ -> Nothing },
     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
     \case { App a -> Just ([], pair term term a); _ -> Nothing },
@@ -2698,7 +2698,7 @@
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
-module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Decode (indexname, sort, typ, term)
 where
 
 import Isabelle.Library
@@ -2720,16 +2720,16 @@
    \([a], b) -> TFree (a, sort b),
    \(a, b) -> TVar (indexname a, sort b)]
 
-typ_body :: T Typ
-typ_body [] = dummyT
-typ_body body = typ body
+var_type :: T Typ
+var_type [] = dummyT
+var_type body = typ body
 
 term :: T Term
 term t =
   t |> variant
    [\([a], b) -> Const (a, list typ b),
-    \([a], b) -> Free (a, typ_body b),
-    \(a, b) -> Var (indexname a, typ_body b),
+    \([a], b) -> Free (a, var_type b),
+    \(a, b) -> Var (indexname a, var_type b),
     \([], a) -> Bound (int a),
     \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
     \([], a) -> App (pair term term a),