src/Pure/Isar/generic_target.ML

   val abbrev: (string * bool -> binding * mixfix -> term * term ->
       term list -> local_theory -> local_theory) ->
     string * bool -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
 
-  val theory_declaration: declaration -> local_theory -> local_theory
+  val theory_declaration: bool -> declaration -> local_theory -> local_theory
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory

   end;
 
 
 (** primitive theory operations **)
 
-fun theory_declaration decl lthy =
+fun theory_declaration syntax decl lthy =
   let
     val global_decl = Morphism.form
       (Morphism.transform (Local_Theory.global_morphism lthy) decl);
   in
     lthy
     |> Local_Theory.background_theory (Context.theory_map global_decl)
     |> Local_Theory.target (Context.proof_map global_decl)
+    |> not syntax ? Context.proof_map (Morphism.form decl)
   end;
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val (const, lthy2) = lthy