# HG changeset patch
# User wenzelm
# Date 1734290549 -3600
# Node ID 5b0fcf59c054f4e7df44aa1893b2fc766b07141b
# Parent  af21a61dadada78ae784a203cc6035e37637c289
tuned;

diff -r af21a61dadad -r 5b0fcf59c054 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Dec 15 20:12:45 2024 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Dec 15 20:22:29 2024 +0100
@@ -511,9 +511,8 @@
                 SOME c => case_fixed c
               | NONE => case_default s))));
 
-val is_marked_entity =
-  unmark_entity {case_class = K true, case_type = K true, case_const = K true,
-    case_fixed = K true, case_default = K false};
+fun is_marked_entity s =
+  is_class s orelse is_type s orelse is_const s orelse is_fixed s;
 
 val dummy_type = Syntax.const (mark_type "dummy");
 val fun_type = Syntax.const (mark_type "fun");