--- 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 *)