# HG changeset patch
# User wenzelm
# Date 1160600119 -7200
# Node ID fade54fde62254b7ee00b2136f7bded4e0ca1b07
# Parent  c4d3fc6e1e64bfefa016626b3c0e33dc4fc2e9ac
is_sid: disallow 'begin' keyword as identifier;

diff -r c4d3fc6e1e64 -r fade54fde622 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 *)