1.1 --- a/src/Pure/Syntax/syntax.ML	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -103,11 +103,6 @@
     1.4      Parse_Print_Rule of 'a * 'a
     1.5    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
     1.6    val update_trfuns:
     1.7 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     1.8 -    (string * ((term list -> term) * stamp)) list *
     1.9 -    (string * ((typ -> term list -> term) * stamp)) list *
    1.10 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
    1.11 -  val update_advanced_trfuns:
    1.12      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.13      (string * ((Proof.context -> term list -> term) * stamp)) list *
    1.14      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    1.15 @@ -651,10 +646,7 @@
    1.16  
    1.17  (** modify syntax **)
    1.18  
    1.19 -fun ext_syntax f decls = update_syntax mode_default (f decls);
    1.20 -
    1.21 -val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns;
    1.22 -val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns;
    1.23 +val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
    1.24  
    1.25  fun update_type_gram add prmode decls =
    1.26    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
    1.27 @@ -662,7 +654,7 @@
    1.28  fun update_const_gram add is_logtype prmode decls =
    1.29    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.30  
    1.31 -val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
    1.32 +val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
    1.33  val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
    1.34  
    1.35