tuned;
authorwenzelm
Sun, 15 Dec 2024 20:22:29 +0100
changeset 81597 5b0fcf59c054
parent 81596 af21a61dadad
child 81598 82cccc88faa5
tuned;
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");