src/Pure/Isar/parse.ML
changeset 42326 e2d22eb4aeb9
parent 42300 0d1cbc1fe579
child 42519 8ac7e96f913b
     1.1 --- a/src/Pure/Isar/parse.ML	Sat Apr 09 15:00:23 2011 +0200
     1.2 +++ b/src/Pure/Isar/parse.ML	Sat Apr 09 23:29:50 2011 +0200
     1.3 @@ -15,7 +15,8 @@
     1.4    val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
     1.5    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
     1.6    val not_eof: Token.T parser
     1.7 -  val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
     1.8 +  val position: 'a parser -> ('a * Position.T) parser
     1.9 +  val inner_syntax: 'a parser -> string parser
    1.10    val command: string parser
    1.11    val keyword: string parser
    1.12    val short_ident: string parser