--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 17:35:53 2024 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 21:47:20 2024 +0100
@@ -1123,8 +1123,8 @@
@{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
+ @{command_def "translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "no_translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\
\end{tabular}