--- a/src/HOL/Proofs/ex/XML_Data.thy Sun Jul 14 15:56:58 2024 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Jul 14 16:07:03 2024 +0200
@@ -48,11 +48,11 @@
text \<open>Some fairly large proof:\<close>
ML_val \<open>
- val xml = export_proof thy1 @{thm abs_less_iff};
+ val xml = export_proof thy1 @{thm Int.times_int.abs_eq};
val thm = import_proof thy1 xml;
- val xml_size = size (YXML.string_of_body xml);
- \<^assert> (xml_size > 100000);
+ val xml_size = Bytes.length (YXML.bytes_of_body xml);
+ \<^assert> (xml_size > 10000000);
\<close>
end