--- a/src/Pure/Isar/outer_lex.ML Tue Jun 27 00:02:01 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML Tue Jun 27 20:35:31 2000 +0200
@@ -106,8 +106,6 @@
fun keyword_with pred (Token (_, (Keyword, x))) = pred x
| keyword_with _ _ = false;
-fun name_of (Token (_, (k, _))) = str_of_kind k;
-
fun is_proper (Token (_, (Space, _))) = false
| is_proper (Token (_, (Comment, _))) = false
| is_proper _ = true;
@@ -132,7 +130,10 @@
| is_indent _ = false;
-(* value of token *)
+(* name and value of token *)
+
+fun name_of (tok as Token (_, (k, x))) =
+ if is_semicolon tok then "terminator" else str_of_kind k ^ " " ^ quote x;
fun val_of (Token (_, (_, x))) = x;
--- 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;