# HG changeset patch
# User wenzelm
# Date 1184879935 -7200
# Node ID 8c6f2e7bfdb4734526b712826b5169de8b9c82b4
# Parent  743f34b12f676db0ca8558702530212555714b56
adapted ThyHeader.read;

diff -r 743f34b12f67 -r 8c6f2e7bfdb4 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},