use smaller example that fits into 64MB string limit of Poly/ML x86 platform;

--- 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