--- a/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 15:58:55 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 16:04:44 2024 +0200
@@ -202,10 +202,6 @@
fun get_notation_markup ctxt =
get_property NONE (SOME Markup.notation0) (SOME o parse_notation ctxt) Markup.notationN;
-fun get_expression_markup ctxt =
- get_property NONE (SOME Markup.expression0) (SOME o Markup_Kind.check_expression ctxt)
- Markup.expressionN;
-
end;
@@ -250,9 +246,7 @@
let
val props = read_properties ss;
- val more_markups =
- the_list (get_notation_markup ctxt props) @
- the_list (get_expression_markup ctxt props);
+ val more_markups = the_list (get_notation_markup ctxt props);
val markup_name = get_string Markup.markupN props;
val markup_props = props |> map_filter (fn (a, opt_b) =>