--- a/src/Pure/Isar/parse.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Isar/parse.ML Fri Mar 08 17:05:23 2019 +0100
@@ -42,8 +42,6 @@
val underscore: string parser
val maybe: 'a parser -> 'a option parser
val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser
- val tag_name: string parser
- val tags: string list parser
val opt_keyword: string -> bool parser
val opt_bang: bool parser
val begin: string parser
@@ -227,9 +225,6 @@
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
val real = float_number >> Value.parse_real || int >> Real.fromInt;
-val tag_name = group (fn () => "tag name") (short_ident || string);
-val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
-
fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
val opt_bang = Scan.optional ($$$ "!" >> K true) false;