diff -r c6ce90275c3d -r 3760a7d21980 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Sep 23 10:56:25 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Sep 23 11:08:30 2024 +0200
@@ -570,11 +570,6 @@
     (Array.nth Estate j);
 
 
-fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
-  if Lexicon.valued_token c orelse id <> ""
-  then (A, j, Tip c :: ts, sa, id, i)
-  else (A, j, ts, sa, id, i);
-
 fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) =
   (A, j, tt @ ts, sa, id, i);
 
@@ -625,10 +620,14 @@
               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
-          | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
-              processS used States
-                (S :: Si,
-                  if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii)
+          | (A, prec, ts, Terminal a :: sa, id, j) => (*scanner operation*)
+              let
+                val Sii' =
+                  if Lexicon.tokens_match_ord (a, c) <> EQUAL then Sii
+                  else (*move dot*)
+                    let val ts' = if Lexicon.valued_token c orelse id <> "" then Tip c :: ts else ts
+                    in (A, prec, ts', sa, id, j) :: Sii end;
+              in processS used States (S :: Si, Sii') end
           | (A, prec, ts, [], id, j) => (*completer operation*)
               let
                 val tt = if id = "" then ts else [Node (id, rev ts)];