# HG changeset patch
# User wenzelm
# Date 1565616281 -7200
# Node ID 5b35d46c994fef45a736cfadebe616c6116b28d4
# Parent  a829207b32a31dcfcf03f6c2d21a2e30881358eb
more direct/compact export of proof terms;

diff -r a829207b32a3 -r 5b35d46c994f src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Aug 12 15:22:32 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Aug 12 15:24:41 2019 +0200
@@ -2009,12 +2009,29 @@
 
 fun clean_proof thy = rew_proof thy #> shrink_proof;
 
+
+local open XML.Encode Term_XML.Encode in
+
+fun proof prf = prf |> variant
+ [fn MinProof => ([], []),
+  fn PBound a => ([int_atom a], []),
+  fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
+  fn a % SOME b => ([], pair proof term (a, b)),
+  fn a %% b => ([], pair proof proof (a, b)),
+  fn Hyp a => ([], term a),
+  fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
+  fn OfClass (T, c) => ([c], typ T),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
+  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
+
+fun encode_export prop prf = pair term proof (prop, prf);
+
+end;
+
 fun export_proof thy i prop prf =
   let
-    val xml =
-      reconstruct_proof thy prop prf
-      |> term_of {thm_const = K o string_of_int, axm_const = axm_const_default}
-      |> Term_XML.Encode.term;
+    val xml = reconstruct_proof thy prop prf |> encode_export prop;
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params