src/Pure/Thy/export_theory.ML
changeset 70015 c8e08d8ffb93
parent 69996 8f2d3a27aff0
child 70384 8ce08b154aa1
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Mar 30 12:07:31 2019 +0100
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Mar 30 20:54:47 2019 +0100
     1.3 @@ -172,7 +172,7 @@
     1.4      if Options.bool (#options context) "export_theory" then f context thy else ()));
     1.5  
     1.6  fun export_body thy name body =
     1.7 -  Export.export thy (Path.make ["theory", name])
     1.8 +  Export.export thy (Path.binding0 (Path.make ["theory", name]))
     1.9      (Buffer.chunks (YXML.buffer_body body Buffer.empty));
    1.10  
    1.11