src/Pure/Isar/local_theory.ML

   val full_name: local_theory -> binding -> string
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val standard_morphism_theory: local_theory -> morphism
-  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
+  val standard_form: local_theory -> Proof.context -> 'a Morphism.entity -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context

   val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> Attrib.fact list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
+  val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_fn ->
+    local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory

  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
-  declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
+  declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+    local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list};
 
 type lthy =

 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define false;
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
-val declaration = operation2 #declaration;
+fun declaration args = operation2 #declaration args o Morphism.entity;
 val theory_registration = operation1 #theory_registration;
 fun locale_dependency registration =
   assert_bottom #> operation1 #locale_dependency registration;