diff -r 36da6a3c79d6 -r 2309ac831dd4 src/HOL/Proofs/ex/XML_Data.thy
--- 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