# 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 *)