src/Pure/Thy/export.ML

 *)
 
 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 =
 struct
 

   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
     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;