tuned;
authorwenzelm
Mon, 20 Sep 2021 21:56:10 +0200
changeset 74332 78c1699c7672
parent 74331 b9a3d2fb53e0
child 74333 a9b20bc32fa6
tuned;
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