diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 20 17:18:44 2023 +0200
@@ -49,7 +49,7 @@
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
-  val internal_declaration: Morphism.declaration -> thms
+  val internal_declaration: Morphism.declaration_entity -> thms
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser