--- a/src/Pure/Pure.thy Mon Sep 20 15:27:00 2021 +0200
+++ b/src/Pure/Pure.thy Mon Sep 20 20:22:32 2021 +0200
@@ -386,12 +386,12 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
+ >> (Toplevel.theory o uncurry (Sign.syntax_cmd true)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
+ >> (Toplevel.theory o uncurry (Sign.syntax_cmd false)));
val trans_pat =
Scan.optional