src/Pure/ProofGeneral/pgip_parser.ML
changeset 27353 71c4dd53d4cb
parent 24192 4eccd4bb8b64
child 27664 0e7a7fcd403b
     1.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
     1.6    | parse_command name text =
     1.7 -      (case OuterSyntax.command_keyword name of
     1.8 +      (case OuterKeyword.command_keyword name of
     1.9          NONE => [D.Unparseable {text = text}]
    1.10        | SOME k =>
    1.11            (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of