diff -r efb98d27dc1a -r cda018294515 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -21,7 +21,7 @@
 fun thy_begin text =
   (case try (Thy_Header.read Position.none) text of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
-  | SOME (name, imports, _) =>
+  | SOME {name, imports, ...} =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];