diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/sessions.ML	Tue Nov 27 21:07:39 2018 +0100
@@ -22,7 +22,7 @@
 val global =
   Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false;
 
-val theory_entry = Parse.position Parse.theory_name --| global;
+val theory_entry = Parse.theory_name --| global;
 
 val theories =
   Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
@@ -46,15 +46,15 @@
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
   Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
   (Parse.$$$ "=" |--
-    Parse.!!! (Scan.option (Parse.position Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
+    Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
       Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
       Scan.optional (Parse.$$$ "sessions" |--
-        Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
+        Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
       Scan.repeat theories --
       Scan.repeat document_files --
       Scan.repeat export_files))
-  >> (fn (((session, _), dir),
+  >> (fn ((((session, _), _), dir),
           (((((((parent, descr), options), sessions), theories), document_files), export_files))) =>
     Toplevel.keep (fn state =>
       let