adapted ThyHeader.read;
authorwenzelm
Thu, 19 Jul 2007 23:18:55 +0200
changeset 23868 8c6f2e7bfdb4
parent 23867 743f34b12f67
child 23869 c886d9897237
adapted ThyHeader.read;
src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu Jul 19 23:18:54 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Jul 19 23:18:55 2007 +0200
@@ -21,7 +21,7 @@
 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
-  (case try ThyHeader.read (Source.of_string text, Position.none) of
+  (case try (ThyHeader.read Position.none) (Source.of_string text) of
     NONE => [D.Unparseable {text = text}]
   | SOME (name, imports, _) =>
       [D.Opentheory {thyname = name, parentnames = imports, text = text},