src/Pure/Thy/thy_info.scala

--- a/src/Pure/Thy/thy_info.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -44,14 +44,10 @@
 
     def deps: List[Dep] = rev_deps.reverse
 
-    def thy_load_commands: List[String] =
-      (for ((cmd, Some(((Keyword.THY_LOAD, _), _))) <- keywords) yield cmd) :::
-        thy_load.base_syntax.thy_load_commands
-
     def loaded_theories: Set[String] =
       (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
 
-    def syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+    def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
 
   private def require_thys(initiators: List[Document.Node.Name],
@@ -66,8 +62,9 @@
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
+        val syntax = required.make_syntax
         val header =
-          try { thy_load.check_thy(name) }
+          try { thy_load.check_thy(syntax, name) }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +