# HG changeset patch
# User wenzelm
# Date 1717958850 -7200
# Node ID 31df11a23d6efe72359648b7578dd7108a7e90b9
# Parent  6d091c0c252e3c12c1cd238b491997efaa4e93c8
clarified signature: more explicit operations;

diff -r 6d091c0c252e -r 31df11a23d6e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jun 09 20:37:39 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jun 09 20:47:30 2024 +0200
@@ -395,7 +395,7 @@
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
 and thm consts (a, thm_node) =
-  pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts))))
+  pair int (pair string (pair Thm_Name.encode (pair (term consts) (proof_body consts))))
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
@@ -463,7 +463,7 @@
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
-      pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts)))) x
+      pair int (pair string (pair Thm_Name.decode (pair (term consts) (proof_body consts)))) x
   in (a, make_thm_node b c d (Future.value e) no_export) end;
 
 in
diff -r 6d091c0c252e -r 31df11a23d6e src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Sun Jun 09 20:37:39 2024 +0200
+++ b/src/Pure/thm_name.ML	Sun Jun 09 20:47:30 2024 +0200
@@ -26,6 +26,8 @@
   val print_suffix: T -> string
   val print: T -> string
   val short: T -> string
+  val encode: T XML.Encode.T
+  val decode: T XML.Decode.T
 end;
 
 structure Thm_Name: THM_NAME =
@@ -104,4 +106,10 @@
   if name = "" orelse index = 0 then name
   else name ^ "_" ^ string_of_int index;
 
+
+(* XML data representation *)
+
+val encode = let open XML.Encode in pair string int end;
+val decode = let open XML.Decode in pair string int end;
+
 end;