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