src/Pure/ProofGeneral/pgip_parser.ML

 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
   (case try (Thy_Header.read Position.none) text of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
-  | SOME {name, imports, ...} =>
-       D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
+  | SOME {name = (name, _), imports, ...} =>
+       D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
 
 fun thy_heading text =
   [D.Closeblock {},
    D.Doccomment {text = text},