# HG changeset patch
# User wenzelm
# Date 1513439826 -3600
# Node ID 99815211970cd6d147e9e2968ef460a960ac5b13
# Parent  03d0c958d65a8d436ebcada6ad69e5dcd733359e
disallow theory name "ROOT";

diff -r 03d0c958d65a -r 99815211970c src/Pure/Thy/sessions.scala
--- 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 }