diff -r 90a44d271683 -r 3837a9ace1c7 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Jun 08 19:36:45 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jun 09 11:40:39 2016 +0200
@@ -47,6 +47,7 @@
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
+  val internal_declaration: declaration -> (thm list * Token.src list) list
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser
@@ -243,6 +244,9 @@
   internal_attribute_name ::
     [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
 
+fun internal_declaration decl =
+  [([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])];
+
 
 (* add/del syntax *)