--- 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