--- a/src/Pure/ProofGeneral/pgip_parser.ML Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Tue Sep 01 14:45:06 2009 +0200
@@ -20,7 +20,7 @@
fun badcmd text = [D.Badcmd {text = text}];
fun thy_begin text =
- (case try (ThyHeader.read Position.none) (Source.of_string text) of
+ (case try (Thy_Header.read Position.none) (Source.of_string text) of
NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
| SOME (name, imports, _) =>
D.Opentheory {thyname = SOME name, parentnames = imports, text = text})