# HG changeset patch
# User wenzelm
# Date 1178638821 -7200
# Node ID decd2ff5f5037068dd449b17de9b34c4a812c9e1
# Parent  d7189dc8939c6d845858ab1fd362fa07934f6d99
is_sid: include '::';

diff -r d7189dc8939c -r decd2ff5f503 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue May 08 17:40:20 2007 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue May 08 17:40:21 2007 +0200
@@ -204,6 +204,7 @@
 
 fun is_sid "begin" = false
   | is_sid ":" = true
+  | is_sid "::" = true
   | is_sid s = is_symid s orelse Syntax.is_identifier s;