--- 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}];