--- 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 *)
--- a/src/Pure/Isar/locale.ML Wed Jun 08 19:36:45 2016 +0200
+++ b/src/Pure/Isar/locale.ML Thu Jun 09 11:40:39 2016 +0200
@@ -612,21 +612,10 @@
(* Declarations *)
-local
-
-fun add_decl loc decl =
- add_thmss loc ""
- [((Binding.empty, [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
- [([Drule.dummy_thm], [])])];
-
-in
-
fun add_declaration loc syntax decl =
syntax ?
Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_decl loc decl;
-
-end;
+ #> add_thmss loc "" [(Attrib.empty_binding, Attrib.internal_declaration decl)];
(*** Reasoning about locales ***)