diff -r e656c5edc352 -r d570d215e380 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Dec 14 17:35:53 2024 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 14 21:47:20 2024 +0100
@@ -430,12 +430,12 @@
     >> (fn (left, (arr, right)) => arr (left, right));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations true));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
+    (Scan.repeat1 trans_line >> Local_Theory.translations_cmd true);
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations false));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
+    (Scan.repeat1 trans_line >> Local_Theory.translations_cmd false);
 
 in end\<close>