# HG changeset patch # User wenzelm # Date 1517323201 -3600 # Node ID f0b2cc2ad4640750c5578107f6cc53b946f05b69 # Parent 99c08d541a7aef4732d6a7c2053dcb35e2163cda prefer specific tokens_subtract: subtle change of comparison via tokens_match; diff -r 99c08d541a7a -r f0b2cc2ad464 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Jan 30 15:15:51 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Tue Jan 30 15:40:01 2018 +0100 @@ -126,7 +126,7 @@ let val ((to_nts, to_tks), ps) = Array.sub (prods, to); - val new_tks = subtract (op =) to_tks from_tks; (*added lookahead tokens*) + val new_tks = tokens_subtract to_tks from_tks; (*added lookahead tokens*) val _ = Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps)); in copy_lookahead tos (if null new_tks then added else (to, new_tks) :: added) @@ -184,7 +184,7 @@ val new_tks = the_list tk |> fold (tokens_union o starts_for_nt) nts - |> subtract (op =) l_starts; + |> tokens_subtract l_starts; val added_tks' = tokens_union added_tks new_tks;