# HG changeset patch
# User clasohm
# Date 830864432 -7200
# Node ID 19fe0ab646b480568f32f0780a8a937de5708549
# Parent  35045774bc1ef38b4aa2b3eede510085cd999fc2
changed ident_no_colon so that it forbids postfix "=", too

diff -r 35045774bc1e -r 19fe0ab646b4 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Apr 30 12:40:09 1996 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue Apr 30 13:40:32 1996 +0200
@@ -231,14 +231,14 @@
 
 (* types *)
 
-(*Parse an identifier, but only if it is not followed by colons or a comma;
+(*Parse an identifier, but only if it is not followed by "::", "=" or ",";
   the exclusion of a postfix comma can be controlled to allow expressions
   like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
 fun ident_no_colon _ [] = eof_err()
   | ident_no_colon allow_comma ((Ident, s, n) :: (rest as (Keyword, s2, n2) ::
                                 toks)) =
-      if s2 = "::" orelse (not allow_comma andalso s2 = ",") then
-        syn_err (name_of_kind Ident) (quote s2) n2
+      if s2 = "::" orelse s2 = "=" orelse (not allow_comma andalso s2 = ",")
+      then syn_err (name_of_kind Ident) (quote s2) n2
       else (s, rest)
   | ident_no_colon _ ((Ident, s, n) :: toks) = (s, toks)
   | ident_no_colon _ ((k, s, n) :: _) =