# HG changeset patch
# User wenzelm
# Date 1517395615 -3600
# Node ID 77d497947fc773735819a2931b74aca42369740d
# Parent  679253fef27751efa334571f1b25a80079094aff
tuned;

diff -r 679253fef277 -r 77d497947fc7 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Wed Jan 31 11:40:26 2018 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Wed Jan 31 11:46:55 2018 +0100
@@ -38,13 +38,15 @@
 fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan);
 fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);
 
-val tfree = Scan.some (fn Lexicon.Token (Lexicon.Type_Ident, s, _) => SOME s | _ => NONE);
-val ident = Scan.some (fn Lexicon.Token (Lexicon.Ident, s, _) => SOME s | _ => NONE);
+fun kind k =
+  Scan.some (fn tok =>
+    if Lexicon.kind_of_token tok = k then SOME (Lexicon.str_of_token tok) else NONE);
 
-val var = Scan.some (fn Lexicon.Token (Lexicon.Var, s, _) =>
-  SOME (Lexicon.read_indexname (unprefix "?" s)) | _ => NONE);
+val tfree = kind Lexicon.Type_Ident;
+val ident = kind Lexicon.Ident;
+val var = kind Lexicon.Var >> (Lexicon.read_indexname o unprefix "?");
+val long_ident = kind Lexicon.Long_Ident;
 
-val long_ident = Scan.some (fn Lexicon.Token (Lexicon.Long_Ident, s, _) => SOME s | _ => NONE);
 val const = long_ident || ident;