# HG changeset patch
# User wenzelm
# Date 1508936068 -7200
# Node ID 1f93e376aeb68132f1138a319366f4d90070fbfb
# Parent  ec2b50aeb0dd5175059edf70cce83a385dbe477c
more explicit check;

diff -r ec2b50aeb0dd -r 1f93e376aeb6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Oct 25 14:39:22 2017 +0200
+++ b/src/Pure/General/symbol.scala	Wed Oct 25 14:54:28 2017 +0200
@@ -60,6 +60,8 @@
     else char_symbols(c.toInt)
   }
 
+  def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
+
 
   /* symbol matching */
 
diff -r ec2b50aeb0dd -r 1f93e376aeb6 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Oct 25 14:39:22 2017 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Oct 25 14:54:28 2017 +0200
@@ -166,7 +166,11 @@
           (minor + name, major)
         else (minor, major + name)
       val load_commands1 =
-        if (kind == THY_LOAD) load_commands + (name -> exts)
+        if (kind == THY_LOAD) {
+          if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
+            error("Bad theory load command " + quote(name))
+          load_commands + (name -> exts)
+        }
         else load_commands
       new Keywords(minor1, major1, kinds1, load_commands1)
     }