# HG changeset patch
# User wenzelm
# Date 948917560 -3600
# Node ID 3243f2261d4bda29b3b9eff7d6e795f8b03639e1
# Parent  cdd5386eb6fe9451ab129a65def019daf589d0f2
'name' etc. include 'number';
attrib: include keyword_sid as name;

diff -r cdd5386eb6fe -r 3243f2261d4b src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Jan 26 21:10:27 2000 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Jan 26 21:12:40 2000 +0100
@@ -154,9 +154,9 @@
 
 (* names and text *)
 
-val name = group "name declaration" (short_ident || sym_ident || string);
-val xname = group "name reference" (short_ident || long_ident || sym_ident || string);
-val text = group "text" (short_ident || long_ident || sym_ident || string || verbatim);
+val name = group "name declaration" (short_ident || sym_ident || string || number);
+val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
+val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 
 
 (* formal comments *)
@@ -182,8 +182,8 @@
 
 (* types *)
 
-val typ =
-  group "type" (short_ident || long_ident || sym_ident || type_ident || type_var || string);
+val typ = group "type"
+  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
 
 val type_args =
   type_ident >> single ||
@@ -243,6 +243,7 @@
 (* arguments *)
 
 fun keyword_symid is_symid = Scan.one (OuterLex.keyword_with is_symid) >> OuterLex.val_of;
+val keyword_sid = keyword_symid OuterLex.is_sid;
 
 fun atom_arg is_symid blk =
   group "argument"
@@ -266,7 +267,7 @@
 
 (* theorem specifications *)
 
-val attrib = position (xname -- !!! (args OuterLex.is_sid false)) >> Args.src;
+val attrib = position ((xname || keyword_sid) -- !!! (args OuterLex.is_sid false)) >> Args.src;
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];