src/Tools/Code/code_runtime.ML
changeset 70011 9dde788b0128
parent 69742 170daa8170be
child 70022 49e178cbf923
--- a/src/Tools/Code/code_runtime.ML	Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Mar 29 13:42:17 2019 +0100
@@ -780,7 +780,7 @@
     (Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
       ::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
     -- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
-    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.name)
+    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.embedded)
     >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
       (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));