src/Pure/Syntax/parser.ML
changeset 40959 49765c1104d4
parent 38875 c7a66b584147
child 41378 55286df6a423
--- a/src/Pure/Syntax/parser.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -841,7 +841,7 @@
     val start_tag =
       (case Symtab.lookup tags startsymbol of
         SOME tag => tag
-      | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
+      | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol));
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);