--- 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;