| changeset 77741 | 1951f6470792 |
| parent 77723 | b761c91c2447 |
| child 77818 | d1ad58e5fc95 |
--- a/src/Pure/Syntax/parser.ML Wed Mar 29 12:02:34 2023 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Mar 29 12:05:56 2023 +0200 @@ -46,7 +46,7 @@ fun nts_fold f (nts: nts) = Intset.fold f nts; fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1; fun nts_is_empty (nts: nts) = Intset.is_empty nts; -fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Intset.is_single nts; +fun nts_is_unique (nts: nts) = Intset.size nts <= 1; (* tokens *)