# HG changeset patch
# User wenzelm
# Date 1430343047 -7200
# Node ID ccf9241af2170deb8cae0c63855df98f61fb124a
# Parent  76853162a87e2c383f01f5ea2663454fa0dca2cb
use smaller example that fits into 64MB string limit of Poly/ML x86 platform;

diff -r 76853162a87e -r ccf9241af217 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Wed Apr 29 23:26:11 2015 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Wed Apr 29 23:30:47 2015 +0200
@@ -57,9 +57,9 @@
 text {* Some fairly large proof: *}
 
 ML_val {*
-  val xml = export_proof @{thm Int.times_int.abs_eq};
+  val xml = export_proof @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
-  @{assert} (size (YXML.string_of_body xml) > 50000000);
+  @{assert} (size (YXML.string_of_body xml) > 1000000);
 *}
 
 end