# HG changeset patch
# User wenzelm
# Date 1721309196 -7200
# Node ID 9c6cfac291f4f81f765d86a9c344f91086e0d21f
# Parent  b1b53f6a08fa2f981b3ee1fd5208cbe985aab05c
clarified signature;

diff -r b1b53f6a08fa -r 9c6cfac291f4 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Thu Jul 18 12:08:08 2024 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Thu Jul 18 15:26:36 2024 +0200
@@ -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 b1b53f6a08fa -r 9c6cfac291f4 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Thu Jul 18 12:08:08 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Thu Jul 18 15:26:36 2024 +0200
@@ -310,7 +310,7 @@
         (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;
 
diff -r b1b53f6a08fa -r 9c6cfac291f4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jul 18 12:08:08 2024 +0200
+++ b/src/Pure/proofterm.ML	Thu Jul 18 15:26:36 2024 +0200
@@ -65,12 +65,12 @@
   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 encode: theory -> proof XML.Encode.T
+  val encode_body: theory -> proof_body XML.Encode.T
+  val encode_standard_term: theory -> term XML.Encode.T
+  val encode_standard_proof: theory -> proof XML.Encode.T
+  val decode: theory -> proof XML.Decode.T
+  val decode_body: theory -> proof_body XML.Decode.T
 
   val %> : proof * term -> proof
 
@@ -428,10 +428,10 @@
 
 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;
+val encode_standard_term = standard_term o Sign.consts_of;
+val encode_standard_proof = standard_proof o Sign.consts_of;
 
 end;
 
@@ -473,8 +473,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;
 
@@ -2160,13 +2160,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)