--- a/src/Pure/Thy/thy_header.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Wed Apr 13 18:01:05 2016 +0200
@@ -117,7 +117,7 @@
fun imports name =
if name = Context.PureN then Scan.succeed []
- else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
+ else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];