src/Pure/Isar/locale.ML

   val specification_of: theory -> string -> term option * term list
 
   (* Storing results *)
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-  val add_declaration: string -> declaration -> Proof.context -> Proof.context
-  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
+  val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
   val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context

             (registrations_of (Context.Theory thy) loc) thy));
 
 
 (* Declarations *)
 
-fun add_declaration loc decl =
+local
+
+fun add_decl loc decl =
   add_thmss loc ""
     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
-fun add_syntax_declaration loc decl =
-  Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
-  #> add_declaration loc decl;
+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;
 
 
 (*** Reasoning about locales ***)
 
 (* Storage for witnesses, intro and unfold rules *)