# 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') \ - \<^descr> \<^theory_text>\declaration d\ adds the declaration function \d\ of ML type \<^ML_type>\Morphism.declaration_fn\, to the current local theory under construction. In later + \<^descr> \<^theory_text>\declaration d\ adds the declaration function \d\ of ML type \<^ML_type>\Morphism.declaration\, 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 *)