author | wenzelm |
Mon, 20 Sep 2021 21:56:10 +0200 | |
changeset 74332 | 78c1699c7672 |
parent 74331 | b9a3d2fb53e0 |
child 74333 | a9b20bc32fa6 |
--- a/src/Pure/Isar/proof_context.ML Mon Sep 20 20:43:38 2021 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Sep 20 21:56:10 2021 +0200 @@ -1146,9 +1146,9 @@ | NONE => NONE) | const_syntax _ _ = NONE; -fun gen_notation syntax add mode args ctxt = +fun gen_notation make_syntax add mode args ctxt = ctxt |> map_syntax_idents - (Local_Syntax.update_modesyntax ctxt add mode (map_filter (syntax ctxt) args)); + (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args)); in