unused;
authorwenzelm
Fri, 03 Apr 2015 20:04:16 +0200
changeset 59918 d01e6d159c33
parent 59917 9830c944670f
child 59919 fe1d8576b483
unused;
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;