src/Pure/Isar/args.ML
changeset 53168 d998de7f0efc
parent 53113 d9ba3417cb41
child 55033 8e8243975860
--- a/src/Pure/Isar/args.ML	Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Pure/Isar/args.ML	Fri Aug 23 17:01:12 2013 +0200
@@ -25,9 +25,9 @@
   val bang: string parser
   val query_colon: string parser
   val bang_colon: string parser
-  val parens: ('a parser) -> 'a parser
-  val bracks: ('a parser) -> 'a parser
-  val mode: string -> bool context_parser
+  val parens: 'a parser -> 'a parser
+  val bracks: 'a parser -> 'a parser
+  val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
   val name_source: string parser
   val name_source_position: (Symbol_Pos.text * Position.T) parser
@@ -145,7 +145,7 @@
 
 fun parens scan = $$$ "(" |-- scan --| $$$ ")";
 fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
-fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
+fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
 val name_source = named >> Token.source_of;