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