# HG changeset patch
# User wenzelm
# Date 1113670597 -7200
# Node ID 00d637286a694c649bc487854bf39fae660d478e
# Parent  44260d72de35ec5d0a456b58e7ea1b9e102b48a5
added del_modesyntax(_i);

diff -r 44260d72de35 -r 00d637286a69 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Apr 16 18:56:21 2005 +0200
+++ b/src/Pure/theory.ML	Sat Apr 16 18:56:37 2005 +0200
@@ -57,6 +57,8 @@
   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
+  val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
+  val del_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
   val add_trfuns:
     (string * (Syntax.ast list -> Syntax.ast)) list *
     (string * (term list -> term)) list *
@@ -219,6 +221,8 @@
 val add_syntax_i           = ext_sign Sign.add_syntax_i;
 val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
 val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
+val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
+val del_modesyntax_i       = curry (ext_sign Sign.del_modesyntax_i);
 val add_trfuns             = ext_sign Sign.add_trfuns;
 val add_trfunsT            = ext_sign Sign.add_trfunsT;
 val add_advanced_trfuns    = ext_sign Sign.add_advanced_trfuns;