| changeset 9155 | adfa40218e06 |
| parent 9131 | cd17637c917f |
| child 11651 | 201b3f76c7b7 |
--- a/src/Pure/Isar/outer_parse.ML Tue Jun 27 00:02:01 2000 +0200 +++ b/src/Pure/Isar/outer_parse.ML Tue Jun 27 20:35:31 2000 +0200 @@ -85,8 +85,7 @@ fun fail_with s = Scan.fail_with (fn [] => s ^ " expected (past end-of-file!)" - | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ " " ^ - quote (T.val_of tok) ^ T.pos_of tok ^ " was found"); + | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ T.pos_of tok ^ " was found"); fun group s scan = scan || fail_with s;