# HG changeset patch
# User wenzelm
# Date 1152727154 -7200
# Node ID a25c5d2832398377e79c8e5437afd1034663f937
# Parent  ba1676dd35462f2fbdc279b56fcf3b697fb15fa7
removed ':' from category of symbolic identifier chars;

diff -r ba1676dd3546 -r a25c5d283239 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Jul 12 19:59:13 2006 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Wed Jul 12 19:59:14 2006 +0200
@@ -190,7 +190,7 @@
 
 (* scan symbolic idents *)
 
-val sym_chars = explode "!#$%&*+-/:<=>?@^_|~";
+val sym_chars = explode "!#$%&*+-/<=>?@^_|~";
 fun is_sym_char s = s mem sym_chars;
 
 val scan_symid =
@@ -203,7 +203,7 @@
   | SOME ss => forall is_sym_char ss
   | _ => false);
 
-val is_sid = is_symid orf Syntax.is_identifier;
+fun is_sid s = s = ":" orelse is_symid s orelse Syntax.is_identifier s;
 
 
 (* scan strings *)