added remove_trrules(_i);
tuned;

--- a/src/Pure/Syntax/syntax.ML	Tue Mar 14 16:29:38 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 14 16:29:39 2006 +0100
@@ -53,11 +53,14 @@
     (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
-  val extend_trrules_i: ast trrule list -> syntax -> syntax
+  val remove_const_gram: (string -> bool) ->
+    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
   val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
-  val remove_const_gram: (string -> bool) ->
-    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
+  val remove_trrules: Context.generic -> (string -> bool) -> syntax ->
+    (string * string) trrule list -> syntax -> syntax
+  val extend_trrules_i: ast trrule list -> syntax -> syntax
+  val remove_trrules_i: ast trrule list -> syntax -> syntax
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val merge_syntaxes: syntax -> syntax -> syntax
   val basic_syn: syntax
@@ -442,6 +445,8 @@
   | print_rule (ParsePrintRule pats) = SOME (swap pats);
 
 
+local
+
 fun check_rule (rule as (lhs, rhs)) =
   (case Ast.rule_error rule of
     SOME msg =>
@@ -467,13 +472,21 @@
     cat_error msg ("The error(s) above occurred in translation pattern " ^
       quote str);
 
-
 fun prep_rules rd_pat raw_rules =
   let val rules = map (map_trrule rd_pat) raw_rules in
     (map check_rule (List.mapPartial parse_rule rules),
       map check_rule (List.mapPartial print_rule rules))
   end
 
+in
+
+val cert_rules = prep_rules I;
+
+fun read_rules context is_logtype syn =
+  prep_rules (read_pattern context is_logtype syn);
+
+end;
+
 
 
 (** pretty terms, typs, sorts **)
@@ -494,7 +507,7 @@
 
 
 
-(** extend syntax **)
+(** modify syntax **)
 
 fun ext_syntax' f is_logtype prmode decls = extend_syntax prmode (f is_logtype decls);
 fun ext_syntax f = ext_syntax' (K f) (K false) default_mode;
@@ -505,15 +518,18 @@
 val extend_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
 val extend_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
 val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
-val extend_trrules_i       = ext_syntax SynExt.syn_ext_rules o prep_rules I;
-
-fun extend_trrules context is_logtype syn rules =
-  ext_syntax' (K SynExt.syn_ext_rules) (K false) default_mode
-    (prep_rules (read_pattern context is_logtype syn) rules);
 
 fun remove_const_gram is_logtype prmode decls =
   remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
 
+fun extend_trrules context is_logtype syn =
+  ext_syntax SynExt.syn_ext_rules o read_rules context is_logtype syn;
+
+fun remove_trrules context is_logtype syn =
+  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules context is_logtype syn;
+
+val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
+val remove_trrules_i = remove_syntax default_mode o SynExt.syn_ext_rules o cert_rules;
 
 
 (*export parts of internal Syntax structures*)