src/Pure/sign.ML
changeset 2385 73d1435aa729
parent 2359 97b88cafe1e8
child 2586 c7a0c0618ca0
     1.1 --- a/src/Pure/sign.ML	Fri Dec 13 17:37:11 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Dec 13 17:37:42 1996 +0100
     1.3 @@ -58,6 +58,8 @@
     1.4      (string * (term list -> term)) list *
     1.5      (string * (term list -> term)) list *
     1.6      (string * (ast list -> ast)) list -> sg -> sg
     1.7 +  val add_trfunsT:
     1.8 +    (string * (typ -> term list -> term)) list -> sg -> sg
     1.9    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    1.10    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.11    val add_name: string -> sg -> sg
    1.12 @@ -549,6 +551,7 @@
    1.13  val add_modesyntax   = extend_sign ext_modesyntax "#";
    1.14  val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
    1.15  val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    1.16 +val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
    1.17  val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
    1.18  val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    1.19