# HG changeset patch
# User wenzelm
# Date 1547402596 -3600
# Node ID cf50cee2adee95f92b7e546fb155ca97426930ed
# Parent  aac49f64051d2e727ffe699dfd1de24905766544
regular export with implicit compression: result is uncompressed;

diff -r aac49f64051d -r cf50cee2adee src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 13 18:48:25 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Jan 13 19:03:16 2019 +0100
@@ -177,9 +177,9 @@
       ());
 
 fun export_to_exports thy width (Singleton (extension, p)) =
-      Export.export_raw thy (generatedN ^ "." ^ extension) [Code_Printer.format [] width p]
+      Export.export thy (generatedN ^ "." ^ extension) [Code_Printer.format [] width p]
   | export_to_exports thy width (Hierarchy code_modules) = (
-      map (fn (names, p) => Export.export_raw thy (Path.implode (Path.make names))
+      map (fn (names, p) => Export.export thy (Path.implode (Path.make names))
         [Code_Printer.format [] width p]) code_modules;
       ());