--- a/src/Pure/proofterm.ML Sat Nov 02 10:43:11 2019 +0100
+++ b/src/Pure/proofterm.ML Sat Nov 02 10:56:53 2019 +0100
@@ -2150,9 +2150,8 @@
val encode_term = encode_standard_term consts;
val encode_proof = encode_standard_proof consts;
in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
- val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
in
- chunks |> Export.export_params
+ YXML.chunks_of_body xml |> Export.export_params
{theory = thy,
binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
executable = false,