# HG changeset patch
# User wenzelm
# Date 1572876874 -3600
# Node ID 4003da7e6a7901945aa025f01941df916096ab79
# Parent  c9f5f724abc0a83bd321090f13eda0b857a38bfd
updated xml_size;

diff -r c9f5f724abc0 -r 4003da7e6a79 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Mon Nov 04 15:06:54 2019 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Mon Nov 04 15:14:34 2019 +0100
@@ -51,7 +51,9 @@
 ML_val \<open>
   val xml = export_proof thy1 @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
-  \<^assert> (size (YXML.string_of_body xml) > 500000);
+
+  val xml_size = size (YXML.string_of_body xml);
+  \<^assert> (xml_size > 400000);
 \<close>
 
 end