# 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");