# HG changeset patch
# User wenzelm
# Date 1570785396 -7200
# Node ID 1fa55b0873bc0babdd9b2bb605c21a6fc3900bfe
# Parent  cb70d84a9f5e8ba34248a78edd555f2b8dbe65bd
tuned signature;

diff -r cb70d84a9f5e -r 1fa55b0873bc src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Oct 10 16:51:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Oct 11 11:16:36 2019 +0200
@@ -271,7 +271,7 @@
       in
         (prop, (deps, proof)) |>
           let open XML.Encode Term_XML.Encode
-          in pair encode_prop (pair (list string) (option (Proofterm.encode_full consts))) end
+          in pair encode_prop (pair (list string) (option (Proofterm.encode_standard consts))) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
diff -r cb70d84a9f5e -r 1fa55b0873bc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 10 16:51:47 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 11:16:36 2019 +0200
@@ -61,7 +61,7 @@
 
   val encode: Consts.T -> proof XML.Encode.T
   val encode_body: Consts.T -> proof_body XML.Encode.T
-  val encode_full: Consts.T -> proof XML.Encode.T
+  val encode_standard: Consts.T -> proof XML.Encode.T
   val decode: Consts.T -> proof XML.Decode.T
   val decode_body: Consts.T -> proof_body XML.Decode.T
 
@@ -351,13 +351,13 @@
     (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 full_proof consts prf = prf |> variant
+fun standard_proof consts prf = prf |> variant
  [fn MinProof => ([], []),
   fn PBound a => ([int_atom a], []),
-  fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)),
-  fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)),
+  fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (standard_proof consts) (b, c)),
+  fn a % SOME b => ([], pair (standard_proof consts) (term consts) (a, b)),
+  fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
   fn Hyp a => ([], term consts a),
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   fn OfClass (T, c) => ([c], typ T),
@@ -369,7 +369,7 @@
 
 val encode = proof;
 val encode_body = proof_body;
-val encode_full = full_proof;
+val encode_standard = standard_proof;
 
 end;
 
@@ -2092,7 +2092,7 @@
 
 fun encode_export consts prop prf =
   let open XML.Encode Term_XML.Encode
-  in pair (term consts) (encode_full consts) (prop, prf) end;
+  in pair (term consts) (encode_standard consts) (prop, prf) end;
 
 fun export_proof thy i prop prf =
   let