--- a/src/Pure/Thy/sessions.scala Sat Dec 16 16:46:01 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Dec 16 16:57:06 2017 +0100
@@ -456,7 +456,12 @@
val session_options = options ++ entry.options
val theories =
- entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
+ entry.theories.map({ case (opts, thys) =>
+ (session_options ++ opts,
+ thys.map({ case ((thy, pos), _) =>
+ if (thy == Sessions.root_name)
+ error("Bad theory name " + quote(thy) + Position.here(pos))
+ else (thy, pos) })) })
val global_theories =
for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }