--- a/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:37:27 2007 +0200
+++ b/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:39:29 2007 +0200
@@ -96,7 +96,7 @@
         let
             val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
         in
-            [D.Opentheory { thyname=thyname, 
+            [D.Opentheory { thyname=SOME thyname, 
 			    parentnames = imports,
 			    text = str },
 	     D.Openblock { metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody }]