# HG changeset patch
# User wenzelm
# Date 1660997020 -7200
# Node ID e4ada7b9e328732fe2b4e6266a2219d8e6ffcc82
# Parent  b327e5d5d6b4a79047233d07146672fd87f1ce18
more thorough check, without path name artifacts (e.g. "./README");

diff -r b327e5d5d6b4 -r e4ada7b9e328 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 20 13:45:47 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 14:03:40 2022 +0200
@@ -570,8 +570,9 @@
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts,
             thys.map({ case ((thy, pos), _) =>
-              if (illegal_theory(thy)) {
-                error("Illegal theory name " + quote(thy) + Position.here(pos))
+              val thy_name = Thy_Header.import_name(thy)
+              if (illegal_theory(thy_name)) {
+                error("Illegal theory name " + quote(thy_name) + Position.here(pos))
               }
               else (thy, pos) })) })