is_sid: disallow 'begin' keyword as identifier;
authorwenzelm
Wed, 11 Oct 2006 22:55:19 +0200
changeset 20982 fade54fde622
parent 20981 c4d3fc6e1e64
child 20983 d4500b9b220e
is_sid: disallow 'begin' keyword as identifier;
src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Oct 11 22:55:18 2006 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Wed Oct 11 22:55:19 2006 +0200
@@ -202,7 +202,9 @@
   | SOME ss => forall is_sym_char ss
   | _ => false);
 
-fun is_sid s = s = ":" orelse is_symid s orelse Syntax.is_identifier s;
+fun is_sid "begin" = false
+  | is_sid ":" = true
+  | is_sid s = is_symid s orelse Syntax.is_identifier s;
 
 
 (* scan strings *)