diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Isar/parse.ML
--- 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;