src/Pure/Pure.thy
changeset 70055 36fb663145e5
parent 70054 a884b2967dd7
child 70056 25c0ad612d62
--- a/src/Pure/Pure.thy	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 04 20:45:55 2019 +0200
@@ -157,7 +157,7 @@
       (Parse.and_list files_in --
         Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
         Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
-        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("compiled", Position.none) --
+        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("", Position.none) --
         (Parse.where_ |-- Parse.!!! Parse.ML_source)
         >> (fn ((((args, external), export), export_prefix), source) =>
           Toplevel.keep (fn st =>