src/Pure/Thy/export.ML
changeset 68167 327bb0f5f768
parent 68146 d23af2dbb4e7
child 69627 3e26471d6d01
     1.1 --- a/src/Pure/Thy/export.ML	Sun May 13 16:05:29 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.ML	Sun May 13 16:26:01 2018 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      name = check_name name,
     1.5      compress = compress} body;
     1.6  
     1.7 -fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body;
     1.8 +val export = gen_export true;
     1.9  val export_raw = gen_export false;
    1.10  
    1.11  end;