# HG changeset patch
# User wenzelm
# Date 1465465239 -7200
# Node ID 3837a9ace1c7a36b371ae0e1a33c323be69988fe
# Parent  90a44d2716837bef7fb1579ca17ea8d8c138cc34
tuned;

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 *)
 
diff -r 90a44d271683 -r 3837a9ace1c7 src/Pure/Isar/locale.ML
--- 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 ***)