# HG changeset patch # User wenzelm # Date 848405015 -3600 # Node ID a9419797e196698e72e9b3d80a36c622cf320e46 # Parent c5a7c72746ac9bf3f0a7e2a15269bed84fc63b6a added add_modesyntax(_i); diff -r c5a7c72746ac -r a9419797e196 src/Pure/theory.ML --- a/src/Pure/theory.ML Mon Nov 18 17:33:35 1996 +0100 +++ b/src/Pure/theory.ML Tue Nov 19 13:03:35 1996 +0100 @@ -36,6 +36,8 @@ val add_consts_i : (string * typ * mixfix) list -> theory -> theory val add_syntax : (string * string * mixfix) list -> theory -> theory val add_syntax_i : (string * typ * mixfix) list -> theory -> theory + val add_modesyntax : string -> (string * string * mixfix) list -> theory -> theory + val add_modesyntax_i : string -> (string * typ * mixfix) list -> theory -> theory val add_trfuns : (string * (Syntax.ast list -> Syntax.ast)) list * (string * (term list -> term)) list * @@ -59,7 +61,8 @@ structure Theory : THEORY = struct -(*** Theories ***) + +(** datatype theory **) datatype theory = Theory of { @@ -129,21 +132,23 @@ fun ext_sg extfun decls (thy as Theory {sign, ...}) = ext_thy thy (extfun decls sign) []; -val add_classes = ext_sg Sign.add_classes; -val add_classrel = ext_sg Sign.add_classrel; -val add_defsort = ext_sg Sign.add_defsort; -val add_types = ext_sg Sign.add_types; -val add_tyabbrs = ext_sg Sign.add_tyabbrs; -val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; -val add_arities = ext_sg Sign.add_arities; -val add_consts = ext_sg Sign.add_consts; -val add_consts_i = ext_sg Sign.add_consts_i; -val add_syntax = ext_sg Sign.add_syntax; -val add_syntax_i = ext_sg Sign.add_syntax_i; -val add_trfuns = ext_sg Sign.add_trfuns; -val add_trrules = ext_sg Sign.add_trrules; -val add_trrules_i = ext_sg Sign.add_trrules_i; -val add_thyname = ext_sg Sign.add_name; +val add_classes = ext_sg Sign.add_classes; +val add_classrel = ext_sg Sign.add_classrel; +val add_defsort = ext_sg Sign.add_defsort; +val add_types = ext_sg Sign.add_types; +val add_tyabbrs = ext_sg Sign.add_tyabbrs; +val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; +val add_arities = ext_sg Sign.add_arities; +val add_consts = ext_sg Sign.add_consts; +val add_consts_i = ext_sg Sign.add_consts_i; +val add_syntax = ext_sg Sign.add_syntax; +val add_syntax_i = ext_sg Sign.add_syntax_i; +val add_modesyntax = curry (ext_sg Sign.add_modesyntax); +val add_modesyntax_i = curry (ext_sg Sign.add_modesyntax_i); +val add_trfuns = ext_sg Sign.add_trfuns; +val add_trrules = ext_sg Sign.add_trrules; +val add_trrules_i = ext_sg Sign.add_trrules_i; +val add_thyname = ext_sg Sign.add_name; (* prepare axioms *)