src/Pure/Thy/export_theory.ML
changeset 69784 24bbc4e30e5b
parent 69087 06017b2c4552
child 69988 6fa51a36b7f7
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -161,7 +161,8 @@
     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 ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
     1.8 +  Export.export thy (Path.make ["theory", name])
     1.9 +    (Buffer.chunks (YXML.buffer_body body Buffer.empty));
    1.10  
    1.11  
    1.12  (* presentation *)