# HG changeset patch
# User wenzelm
# Date 1427741471 -7200
# Node ID 49b975c5f58d68d200e41d369c51e61c0672e6a9
# Parent  ffd50fdfc7fa50f0cbf905715a0c4c24d88bf66f
tuned signature;

diff -r ffd50fdfc7fa -r 49b975c5f58d src/Pure/Isar/args.ML
--- 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