src/Pure/Isar/theory_target.ML

       locale_notes loc kind facts #> context_notes kind facts;
 
 
 (* declarations *)
 
-fun term_syntax "" f = LocalTheory.theory (Context.theory_map f)
-  | term_syntax loc f = LocalTheory.target (Locale.add_term_syntax loc (Context.proof_map f));
-
-fun declaration "" f = LocalTheory.theory (Context.theory_map f)
-  | declaration loc f = I;    (* FIXME *)
+(* FIXME proper morphisms *)
+fun decl _ "" f = LocalTheory.theory (Context.theory_map (f Morphism.identity))
+  | decl add loc f = LocalTheory.target (add loc (Context.proof_map o f));
+
+val type_syntax = decl Locale.add_type_syntax;
+val term_syntax = decl Locale.add_term_syntax;
+val declaration = decl Locale.add_declaration;
 
 
 (* init and exit *)
 
 fun begin loc =

    {pretty = pretty loc,
     consts = consts loc,
     axioms = axioms,
     defs = defs,
     notes = notes loc,
+    type_syntax = type_syntax loc,
     term_syntax = term_syntax loc,
     declaration = declaration loc,
     reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),
     exit = LocalTheory.target_of}