changeset 59857 | 49b975c5f58d |
parent 59809 | 87641097d0f3 |
child 60577 | 4c9401fbbdf7 |
--- a/src/Pure/Isar/args.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/Pure/Isar/args.ML Mon Mar 30 20:51:11 2015 +0200 @@ -23,6 +23,7 @@ val maybe: 'a parser -> 'a option parser val cartouche_inner_syntax: string parser val cartouche_input: Input.source parser + val text_token: Token.T parser val text_input: Input.source parser val text: string parser val name_inner_syntax: string parser