# HG changeset patch
# User wenzelm
# Date 1304265909 -7200
# Node ID 8ac7e96f913b33dcc27e092e8a2c8a032e52abfd
# Parent  57367832b81ad3c33424e34ea5af0fd59ac58fb4
tuned;

diff -r 57367832b81a -r 8ac7e96f913b src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun May 01 17:55:29 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Sun May 01 18:05:09 2011 +0200
@@ -114,7 +114,7 @@
 
 fun fail_with s = Scan.fail_with
   (fn [] => s ^ " expected (past end-of-file!)"
-    | (tok :: _) =>
+    | tok :: _ =>
         (case Token.text_of tok of
           (txt, "") =>
             s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"