--- 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.
--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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,
--- 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*)
--- 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;
--- 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 *)