diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/parse.scala	Sat Nov 01 15:01:41 2014 +0100
@@ -39,13 +39,7 @@
               }
             val token = in.first
             if (pred(token)) Success((token, pos), proper(in.rest))
-            else
-              token.text match {
-                case (txt, "") =>
-                  Failure(s + " expected,\nbut " + txt + " was found", in)
-                case (txt1, txt2) =>
-                  Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
-              }
+            else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
           }
         }
       }