# HG changeset patch
# User wenzelm
# Date 1526058213 -7200
# Node ID d23af2dbb4e76938b559b64452e955fdb7deb53d
# Parent  edacd2a050be3834650919ac5c6b86f95d8d4a35
more scalable API;

diff -r edacd2a050be -r d23af2dbb4e7 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Fri May 11 17:27:30 2018 +0200
+++ b/src/Pure/Thy/export.ML	Fri May 11 19:03:33 2018 +0200
@@ -6,8 +6,8 @@
 
 signature EXPORT =
 sig
-  val export: theory -> string -> string -> unit
-  val export_raw: theory -> string -> string -> unit
+  val export: theory -> string -> string list -> unit
+  val export_raw: theory -> string -> string list -> unit
 end;
 
 structure Export: EXPORT =
@@ -31,9 +31,9 @@
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = check_name name,
-    compress = compress} [body];
+    compress = compress} body;
 
-fun export thy name body = gen_export (size body > 60) thy name body;
+fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body;
 val export_raw = gen_export false;
 
 end;