# HG changeset patch
# User wenzelm
# Date 1684595924 -7200
# Node ID dd7bb7f99ad51c084a14e8d61e51af9d850e1e97
# Parent  f0aca0506531c586c935dcd86e482bb016b13c69
tuned signature;

diff -r f0aca0506531 -r dd7bb7f99ad5 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat May 20 16:12:37 2023 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat May 20 17:18:44 2023 +0200
@@ -417,7 +417,7 @@
     @@{command declare} (@{syntax thms} + @'and')
   \<close>
 
-  \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration_fn\<close>, to the current local theory under construction. In later
+  \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration\<close>, to the current local theory under construction. In later
   application contexts, the function is transformed according to the morphisms
   being involved in the interpretation hierarchy.
 
diff -r f0aca0506531 -r dd7bb7f99ad5 src/HOL/Decision_Procs/ferrante_rackoff_data.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sat May 20 17:18:44 2023 +0200
@@ -15,7 +15,7 @@
   val funs: thm -> 
     {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
      whatis: morphism -> cterm -> cterm -> ord,
-     simpset: morphism -> Proof.context -> simpset} -> Morphism.declaration_fn
+     simpset: morphism -> Proof.context -> simpset} -> Morphism.declaration
   val match: Proof.context -> cterm -> entry option
 end;
 
diff -r f0aca0506531 -r dd7bb7f99ad5 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat May 20 17:18:44 2023 +0200
@@ -6,7 +6,7 @@
 
 signature PARTIAL_FUNCTION =
 sig
-  val init: string -> term -> term -> thm -> thm -> thm option -> Morphism.declaration_fn
+  val init: string -> term -> term -> thm -> thm -> thm option -> Morphism.declaration
   val mono_tac: Proof.context -> int -> tactic
   val add_partial_function: string -> (binding * typ option * mixfix) list ->
     Attrib.binding * term -> local_theory -> (term * thm) * local_theory
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/args.ML	Sat May 20 17:18:44 2023 +0200
@@ -37,14 +37,15 @@
   val internal_term: term parser
   val internal_fact: thm list parser
   val internal_attribute: attribute Morphism.entity parser
-  val internal_declaration: Morphism.declaration parser
+  val internal_declaration: Morphism.declaration_entity parser
   val named_source: (Token.T -> Token.src) -> Token.src parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> string option * thm list) -> thm list parser
   val named_attribute: (string * Position.T -> attribute Morphism.entity) ->
     attribute Morphism.entity parser
-  val embedded_declaration: (Input.source -> Morphism.declaration) -> Morphism.declaration parser
+  val embedded_declaration: (Input.source -> Morphism.declaration_entity) ->
+    Morphism.declaration_entity parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 20 17:18:44 2023 +0200
@@ -49,7 +49,7 @@
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
-  val internal_declaration: Morphism.declaration -> thms
+  val internal_declaration: Morphism.declaration_entity -> thms
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat May 20 17:18:44 2023 +0200
@@ -16,7 +16,7 @@
   (*background primitives*)
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
-  val background_declaration: Morphism.declaration -> local_theory -> local_theory
+  val background_declaration: Morphism.declaration_entity -> local_theory -> local_theory
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
   val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) ->
     theory -> theory
@@ -25,7 +25,7 @@
   val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list
   val standard_notes: (int * int -> bool) -> string -> Attrib.fact list ->
     local_theory -> local_theory
-  val standard_declaration: (int * int -> bool) -> Morphism.declaration ->
+  val standard_declaration: (int * int -> bool) -> Morphism.declaration_entity ->
     local_theory -> local_theory
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
@@ -55,7 +55,7 @@
   (*theory target operations*)
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> (term * term) * local_theory
-  val theory_declaration: Morphism.declaration -> local_theory -> local_theory
+  val theory_declaration: Morphism.declaration_entity -> local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
 
   (*locale target primitives*)
@@ -63,7 +63,7 @@
     local_theory -> local_theory
   val locale_target_abbrev: string -> Syntax.mode ->
     (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
-  val locale_target_declaration: string -> bool -> Morphism.declaration ->
+  val locale_target_declaration: string -> bool -> Morphism.declaration_entity ->
     local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
@@ -71,7 +71,7 @@
   (*locale operations*)
   val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> (term * term) * local_theory
-  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
     local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat May 20 17:18:44 2023 +0200
@@ -55,7 +55,7 @@
     (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} -> Morphism.declaration_fn ->
+  val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
     local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
@@ -103,7 +103,7 @@
   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} -> Morphism.declaration ->
+  declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
     local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Sat May 20 17:18:44 2023 +0200
@@ -39,7 +39,7 @@
     term option * term list ->
     thm option * thm option -> thm list ->
     Element.context_i list ->
-    Morphism.declaration list ->
+    Morphism.declaration_entity list ->
     (string * Attrib.fact list) list ->
     (string * morphism) list -> theory -> theory
   val locale_space: theory -> Name_Space.T
@@ -59,7 +59,7 @@
 
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
-  val add_declaration: string -> bool -> Morphism.declaration -> Proof.context -> Proof.context
+  val add_declaration: string -> bool -> Morphism.declaration_entity -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
@@ -152,7 +152,7 @@
   (* dynamic part *)
 
   (*syntax declarations*)
-  syntax_decls: (Morphism.declaration * serial) list,
+  syntax_decls: (Morphism.declaration_entity * serial) list,
   (*theorem declarations*)
   notes: ((string * Attrib.fact list) * serial) list,
   (*locale dependencies (sublocale relation) in reverse order*)
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/Isar/token.ML	Sat May 20 17:18:44 2023 +0200
@@ -30,7 +30,7 @@
     Term of term |
     Fact of string option * thm list |
     Attribute of attribute Morphism.entity |
-    Declaration of Morphism.declaration |
+    Declaration of Morphism.declaration_entity |
     Files of file Exn.result list |
     Output of XML.body option
   val pos_of: T -> Position.T
@@ -198,7 +198,7 @@
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of attribute Morphism.entity |
-  Declaration of Morphism.declaration |
+  Declaration of Morphism.declaration_entity |
   Files of file Exn.result list |
   Output of XML.body option;
 
diff -r f0aca0506531 -r dd7bb7f99ad5 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat May 20 16:12:37 2023 +0200
+++ b/src/Pure/morphism.ML	Sat May 20 17:18:44 2023 +0200
@@ -49,8 +49,8 @@
   val transform_reset_context: morphism -> 'a entity -> 'a entity
   val form: 'a entity -> 'a
   val form_entity: (morphism -> 'a) -> 'a
-  type declaration = (Context.generic -> Context.generic) entity
-  type declaration_fn = morphism -> Context.generic -> Context.generic
+  type declaration = morphism -> Context.generic -> Context.generic
+  type declaration_entity = (Context.generic -> Context.generic) entity
   val binding_morphism: string -> (binding -> binding) -> morphism
   val typ_morphism': string -> (theory -> typ -> typ) -> morphism
   val typ_morphism: string -> (typ -> typ) -> morphism
@@ -193,8 +193,8 @@
 fun form (Entity (f, phi)) = f phi;
 fun form_entity f = f identity;
 
-type declaration = (Context.generic -> Context.generic) entity;
-type declaration_fn = morphism -> Context.generic -> Context.generic;
+type declaration = morphism -> Context.generic -> Context.generic;
+type declaration_entity = (Context.generic -> Context.generic) entity;
 
 
 (* concrete morphisms *)