# HG changeset patch
# User wenzelm
# Date 962130931 -7200
# Node ID adfa40218e06f6b7c99969ce9e71eba0dc1e16cb
# Parent  e71460b18988420a2291de436d8fe51bb96dbccc
OuterLex.name_of: include val;

diff -r e71460b18988 -r adfa40218e06 src/Pure/Isar/outer_lex.ML
--- 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;
 
diff -r e71460b18988 -r adfa40218e06 src/Pure/Isar/outer_parse.ML
--- 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;