# HG changeset patch # User wenzelm # Date 1525772193 -7200 # Node ID c925f53fd1f6a13098250d16e400dd073909ec90 # Parent 2277fe496d787f9fc4ba82b5e7e4be3f901fd07c tuned signature; diff -r 2277fe496d78 -r c925f53fd1f6 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Mon May 07 23:08:22 2018 +0200 +++ b/src/Pure/Thy/export.ML Tue May 08 11:36:33 2018 +0200 @@ -7,7 +7,7 @@ signature EXPORT = sig val export: theory -> string -> string -> unit - val export_raw: theory -> string -> string list -> unit + val export_raw: theory -> string -> string -> 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_raw thy name body = gen_export false thy name body; +fun export thy name body = gen_export (size body > 60) thy name body; +val export_raw = gen_export false; end;