# HG changeset patch
# User wenzelm
# Date 1717960598 -7200
# Node ID a828e47c867c669a97ca5ee4d6929d111dc714a6
# Parent  b48768f9567fc100ae3f5866cb1a0f764fd4cd76
clarified data representation: prefer explicit type Thm_Name;

diff -r b48768f9567f -r a828e47c867c src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Sun Jun 09 21:15:27 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Sun Jun 09 21:16:38 2024 +0200
@@ -295,7 +295,7 @@
 
     fun encode_thm thm_id raw_thm =
       let
-        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
+        val deps = map #2 (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = prep_thm raw_thm;
 
         val proof0 =
@@ -311,7 +311,7 @@
           let
             open XML.Encode Term_XML.Encode;
             val encode_proof = Proofterm.encode_standard_proof consts;
-          in triple encode_prop (list string) encode_proof end
+          in triple encode_prop (list Thm_Name.encode) encode_proof end
       end;
 
     fun export_thm (thm_id, thm_name) =
diff -r b48768f9567f -r a828e47c867c src/Pure/Build/export_theory.scala
--- a/src/Pure/Build/export_theory.scala	Sun Jun 09 21:15:27 2024 +0200
+++ b/src/Pure/Build/export_theory.scala	Sun Jun 09 21:16:38 2024 +0200
@@ -346,13 +346,13 @@
 
   sealed case class Thm(
     prop: Prop,
-    deps: List[String],
+    deps: List[Thm_Name],
     proof: Term.Proof)
   extends Content[Thm] {
     override def cache(cache: Term.Cache): Thm =
       Thm(
         prop.cache(cache),
-        deps.map(cache.string),
+        deps.map(cache.thm_name),
         cache.proof(proof))
   }
 
@@ -361,7 +361,7 @@
       { body =>
         import XML.Decode._
         import Term_XML.Decode._
-        val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
+        val (prop, deps, prf) = triple(decode_prop, list(Thm_Name.decode), proof)(body)
         Thm(prop, deps, prf)
       })
 
diff -r b48768f9567f -r a828e47c867c src/Pure/term.scala
--- a/src/Pure/term.scala	Sun Jun 09 21:15:27 2024 +0200
+++ b/src/Pure/term.scala	Sun Jun 09 21:16:38 2024 +0200
@@ -274,6 +274,8 @@
       if (no_cache) x else synchronized { cache_typ(x) }
     def term(x: Term): Term =
       if (no_cache) x else synchronized { cache_term(x) }
+    def thm_name(x: Thm_Name): Thm_Name =
+      if (no_cache) x else synchronized { cache_thm_name(x) }
     def proof(x: Proof): Proof =
       if (no_cache) x else synchronized { cache_proof(x) }