src/Pure/Pure.thy
changeset 81590 e656c5edc352
parent 81534 c32ebdcbe8ca
child 81591 d570d215e380
--- a/src/Pure/Pure.thy	Sat Dec 14 16:58:53 2024 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 14 17:35:53 2024 +0100
@@ -431,11 +431,11 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations true));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations false));
 
 in end\<close>