# HG changeset patch
# User wenzelm
# Date 1517393916 -3600
# Node ID 7b399522d6c191df4311b1fd7e7bd02a52e00238
# Parent  c0f1667c19438e2124da21030bc9a67bdc902688
clarified modules;

diff -r c0f1667c1943 -r 7b399522d6c1 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:09:05 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:18:36 2018 +0100
@@ -28,6 +28,7 @@
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
+  val tokens_match_ord: token * token -> order
   val is_proper: token -> bool
   val mk_eof: Position.T -> token
   val eof: token
@@ -144,6 +145,11 @@
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
 
+fun tokens_match_ord toks =
+  (case apply2 kind_of_token toks of
+    (Literal, Literal) => fast_string_ord (apply2 str_of_token toks)
+  | kinds => token_kind_ord kinds);
+
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 
diff -r c0f1667c1943 -r 7b399522d6c1 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Jan 31 11:09:05 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Jan 31 11:18:36 2018 +0100
@@ -52,17 +52,7 @@
 
 (* tokens *)
 
-fun tokens_match toks =
-  (case apply2 Lexicon.kind_of_token toks of
-    (Lexicon.Literal, Lexicon.Literal) => op = (apply2 Lexicon.str_of_token toks)
-  | kinds => op = kinds);
-
-fun tokens_match_ord toks =
-  (case apply2 Lexicon.kind_of_token toks of
-    (Lexicon.Literal, Lexicon.Literal) => fast_string_ord (apply2 Lexicon.str_of_token toks)
-  | kinds => Lexicon.token_kind_ord kinds);
-
-structure Tokens = Table(type key = Lexicon.token val ord = tokens_match_ord);
+structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
 
 type tokens = Tokens.set;
 val tokens_empty: tokens = Tokens.empty;
@@ -652,7 +642,8 @@
               end
           | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
               processS used States
-                (S :: Si, if tokens_match (a, c) then movedot_term c S :: Sii else Sii)
+                (S :: Si,
+                  if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii)
           | (A, prec, ts, [], id, j) => (*completer operation*)
               let val tt = if id = "" then ts else [Node (id, rev ts)] in
                 if j = i then (*lambda production?*)