# HG changeset patch
# User wenzelm
# Date 1632167770 -7200
# Node ID 78c1699c7672149d4192948287f5ab9d4885d135
# Parent  b9a3d2fb53e019dc2bbfc31b6ab2aaed9e199a88
tuned;

diff -r b9a3d2fb53e0 -r 78c1699c7672 src/Pure/Isar/proof_context.ML
--- 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