--- a/src/Doc/Isar_Ref/Spec.thy Thu May 18 15:34:01 2023 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu May 18 17:21:29 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>declaration\<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_fn\<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.