# HG changeset patch
# User wenzelm
# Date 1428084256 -7200
# Node ID d01e6d159c33b7985535120f6d2619b595771196
# Parent  9830c944670f70861957608fcc4f800c34942a9b
unused;

diff -r 9830c944670f -r d01e6d159c33 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Apr 03 19:56:51 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 03 20:04:16 2015 +0200
@@ -44,7 +44,6 @@
   val maybe: 'a parser -> 'a option parser
   val tag_name: string parser
   val tags: string list parser
-  val opt_unit: unit parser
   val opt_keyword: string -> bool parser
   val opt_bang: bool parser
   val begin: string parser
@@ -230,7 +229,6 @@
 val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
 
-val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
 val opt_bang = Scan.optional ($$$ "!" >> K true) false;