# HG changeset patch
# User wenzelm
# Date 1517404317 -3600
# Node ID 5f86e2a9c59c75156fa5ed6f9af084c46a14c7c4
# Parent  c550e38dd13134b1186bb529b6838a28f8efbef3
tuned;

diff -r c550e38dd131 -r 5f86e2a9c59c src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 14:02:37 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 14:11:57 2018 +0100
@@ -39,11 +39,11 @@
   val stopper: token Scan.stopper
   val terminals: string list
   val is_terminal: string -> bool
+  val get_terminal: string -> token option
   val literal_markup: string -> Markup.T
   val report_of_token: token -> Position.report
   val reported_token_range: Proof.context -> token -> string
   val valued_token: token -> bool
-  val predef_term: string -> token option
   val implode_string: Symbol.symbol list -> string
   val explode_string: string * Position.T -> Symbol_Pos.T list
   val implode_str: Symbol.symbol list -> string
@@ -171,22 +171,28 @@
 val stopper = Scan.stopper (K eof) is_eof;
 
 
-(* terminal arguments *)
+(* terminal symbols *)
 
-val terminal_kinds =
- [("id", Ident),
-  ("longid", Long_Ident),
-  ("var", Var),
-  ("tid", Type_Ident),
-  ("tvar", Type_Var),
-  ("num_token", Num),
-  ("float_token", Float),
-  ("str_token", Str),
-  ("string_token", String),
-  ("cartouche", Cartouche)];
+val terminal_symbols =
+  [("id", Ident),
+   ("longid", Long_Ident),
+   ("var", Var),
+   ("tid", Type_Ident),
+   ("tvar", Type_Var),
+   ("num_token", Num),
+   ("float_token", Float),
+   ("str_token", Str),
+   ("string_token", String),
+   ("cartouche", Cartouche)]
+  |> map (apsnd token_kind_index)
+  |> Symtab.make;
 
-val terminals = map #1 terminal_kinds;
-val is_terminal = member (op =) terminals;
+val terminals = Symtab.keys terminal_symbols;
+val is_terminal = Symtab.defined terminal_symbols;
+fun get_terminal s =
+  (case Symtab.lookup terminal_symbols s of
+    SOME i => SOME (Token (i, s, Position.no_range))
+  | NONE => NONE);
 
 
 (* markup *)
@@ -226,14 +232,6 @@
   not (is_literal tok orelse is_eof tok);
 
 
-(* predef_term *)
-
-fun predef_term s =
-  (case AList.lookup (op =) terminal_kinds s of
-    SOME k => SOME (Token (token_kind_index k, s, Position.no_range))
-  | NONE => NONE);
-
-
 
 (** string literals **)
 
diff -r c550e38dd131 -r 5f86e2a9c59c src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Jan 31 14:02:37 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Jan 31 14:11:57 2018 +0100
@@ -452,7 +452,7 @@
           | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
               let
                 val (nt_count', tags', new_symb) =
-                  (case Lexicon.predef_term s of
+                  (case Lexicon.get_terminal s of
                     NONE =>
                       let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
                       in (nt_count', tags', Nonterminal (s_tag, p)) end