--- a/src/Doc/Isar_Ref/Spec.thy Sat May 20 16:12:37 2023 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sat May 20 17:18:44 2023 +0200
@@ -417,7 +417,7 @@
@@{command declare} (@{syntax thms} + @'and')
\<close>
- \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration_fn\<close>, to the current local theory under construction. In later
+ \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration\<close>, to the current local theory under construction. In later
application contexts, the function is transformed according to the morphisms
being involved in the interpretation hierarchy.