--- 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 [];