diff -r f6ff19188842 -r 03aa1b63af10 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Fri Mar 13 21:35:48 2015 +0100
+++ b/src/Pure/Isar/parse.scala	Sat Mar 14 16:56:11 2015 +0100
@@ -25,31 +25,42 @@
       if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
-    def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
-      new Parser[(Elem, Token.Pos)] {
+    private def proper_position: Parser[Position.T] =
+      new Parser[Position.T] {
+        def apply(raw_input: Input) =
+        {
+          val in = proper(raw_input)
+          val pos =
+            in.pos match {
+              case pos: Token.Pos => pos
+              case _ => Token.Pos.none
+            }
+          Success(if (in.atEnd) pos.position() else pos.position(in.first), in)
+        }
+      }
+
+    def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
+      proper_position ~ parser ^^ { case x ~ y => (y, x) }
+
+    def token(s: String, pred: Elem => Boolean): Parser[Elem] =
+      new Parser[Elem] {
         def apply(raw_input: Input) =
         {
           val in = proper(raw_input)
           if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
           else {
-            val pos =
-              in.pos match {
-                case pos: Token.Pos => pos
-                case _ => Token.Pos.none
-              }
             val token = in.first
-            if (pred(token)) Success((token, pos), proper(in.rest))
+            if (pred(token)) Success(token, proper(in.rest))
             else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
           }
         }
       }
 
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
-      token(s, pred) ^^ { case (tok, _) => tok.content }
+      token(s, pred) ^^ (_.content)
 
-    def command(name: String): Parser[Position.T] =
-      token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
-        { case (tok, pos) => pos.position(tok) }
+    def command(name: String): Parser[String] =
+      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
 
     def $$$(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)