src/Pure/Syntax/syntax.ML
changeset 12073 b4401452928e
parent 11546 2b3f02227c35
child 12094 db9a3ad6e90e
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 06 19:29:06 2001 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 06 19:29:36 2001 +0100
     1.3 @@ -28,19 +28,19 @@
     1.4      PrintRule of 'a * 'a |
     1.5      ParsePrintRule of 'a * 'a
     1.6    type syntax
     1.7 -  val extend_log_types: syntax -> string list -> syntax
     1.8 -  val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
     1.9 -  val extend_const_gram: syntax -> string * bool -> (string * typ * mixfix) list -> syntax
    1.10 -  val extend_consts: syntax -> string list -> syntax
    1.11 -  val extend_trfuns: syntax ->
    1.12 +  val extend_log_types: string list -> syntax -> syntax
    1.13 +  val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
    1.14 +  val extend_const_gram: string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    1.15 +  val extend_consts: string list -> syntax -> syntax
    1.16 +  val extend_trfuns:
    1.17      (string * (ast list -> ast)) list *
    1.18      (string * (term list -> term)) list *
    1.19      (string * (term list -> term)) list *
    1.20 -    (string * (ast list -> ast)) list -> syntax
    1.21 -  val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax
    1.22 -  val extend_tokentrfuns: syntax -> (string * string * (string -> string * real)) list -> syntax
    1.23 -  val extend_trrules: syntax -> (string * string) trrule list -> syntax
    1.24 -  val extend_trrules_i: syntax -> ast trrule list -> syntax
    1.25 +    (string * (ast list -> ast)) list -> syntax -> syntax
    1.26 +  val extend_trfunsT: (string * (bool -> typ -> term list -> term)) list -> syntax -> syntax
    1.27 +  val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    1.28 +  val extend_trrules: (string * string) trrule list -> syntax -> syntax
    1.29 +  val extend_trrules_i: ast trrule list -> syntax -> syntax
    1.30    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.31    val merge_syntaxes: syntax -> syntax -> syntax
    1.32    val type_syn: syntax
    1.33 @@ -474,16 +474,16 @@
    1.34  
    1.35  (** extend syntax (external interfaces) **)
    1.36  
    1.37 -fun ext_syntax mk_syn_ext prmode (syn as Syntax {logtypes, ...}) decls =
    1.38 +fun ext_syntax mk_syn_ext prmode decls (syn as Syntax {logtypes, ...}) =
    1.39    extend_syntax prmode syn (mk_syn_ext logtypes decls);
    1.40  
    1.41  
    1.42 -fun extend_log_types syn logtypes =
    1.43 +fun extend_log_types logtypes syn =
    1.44    extend_syntax ("", true) syn (SynExt.syn_ext_logtypes logtypes);
    1.45  
    1.46  val extend_type_gram = ext_syntax Mixfix.syn_ext_types ("", true);
    1.47  
    1.48 -fun extend_const_gram syn prmode = ext_syntax Mixfix.syn_ext_consts prmode syn;
    1.49 +fun extend_const_gram prmode = ext_syntax Mixfix.syn_ext_consts prmode;
    1.50  
    1.51  val extend_consts = ext_syntax SynExt.syn_ext_const_names ("", true);
    1.52  
    1.53 @@ -493,11 +493,10 @@
    1.54  
    1.55  val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns ("", true);
    1.56  
    1.57 -fun extend_trrules syn rules =
    1.58 -  ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
    1.59 +fun extend_trrules rules syn =
    1.60 +  ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules (read_pattern syn) rules) syn;
    1.61  
    1.62 -fun extend_trrules_i syn rules =
    1.63 -  ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules I rules);
    1.64 +fun extend_trrules_i rules = ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules I rules);
    1.65  
    1.66  
    1.67