src/Pure/Isar/parse.ML

--- a/src/Pure/Isar/parse.ML	Thu Jul 02 00:09:04 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Jul 02 12:33:04 2015 +0200
@@ -23,6 +23,7 @@
   val short_ident: string parser
   val long_ident: string parser
   val sym_ident: string parser
+  val dots: string parser
   val minus: string parser
   val term_var: string parser
   val type_ident: string parser
@@ -220,7 +221,10 @@
   group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
+val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;