src/Pure/sign.ML
changeset 4619 72edc2a9200f
parent 4568 7be03035c553
child 4627 ae95666c71cc
     1.1 --- a/src/Pure/sign.ML	Thu Feb 12 12:36:55 1998 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 12 12:37:53 1998 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4      (string * (bool -> typ -> term list -> term)) list -> sg -> sg
     1.5    val add_tokentrfuns:
     1.6      (string * string * (string -> string * int)) list -> sg -> sg
     1.7 -  val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
     1.8 +  val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
     1.9    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.10    val add_path: string -> sg -> sg
    1.11    val add_space: string * string list -> sg -> sg
    1.12 @@ -801,6 +801,14 @@
    1.13    end;
    1.14  
    1.15  
    1.16 +(* add translation rules *)
    1.17 +
    1.18 +fun ext_trrules (syn, tsig, ctab, (path, spaces), data) args =
    1.19 +  (Syntax.extend_trrules syn
    1.20 +    (map (Syntax.map_trrule (fn (root, str) => (intrn spaces typeK root, str))) args),
    1.21 +      tsig, ctab, (path, spaces), data);
    1.22 +
    1.23 +
    1.24  (* add to syntax *)
    1.25  
    1.26  fun ext_syn extfun (syn, tsig, ctab, names, data) args =
    1.27 @@ -857,7 +865,7 @@
    1.28  val add_trfuns       = extend_sign true (ext_syn Syntax.extend_trfuns) "#";
    1.29  val add_trfunsT      = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
    1.30  val add_tokentrfuns  = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
    1.31 -val add_trrules      = extend_sign true (ext_syn Syntax.extend_trrules) "#";
    1.32 +val add_trrules      = extend_sign true ext_trrules "#";
    1.33  val add_trrules_i    = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
    1.34  val add_path         = extend_sign true ext_path "#";
    1.35  val add_space        = extend_sign true ext_space "#";