src/Pure/sign.ML
changeset 4344 e000b5db4087
parent 4261 e20b9fd85811
child 4489 749600cb5573
     1.1 --- a/src/Pure/sign.ML	Tue Dec 02 12:41:02 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 02 12:41:29 1997 +0100
     1.3 @@ -103,12 +103,12 @@
     1.4    val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
     1.5    val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
     1.6    val add_trfuns:
     1.7 -    (bstring * (ast list -> ast)) list *
     1.8 -    (bstring * (term list -> term)) list *
     1.9 -    (bstring * (term list -> term)) list *
    1.10 -    (bstring * (ast list -> ast)) list -> sg -> sg
    1.11 +    (string * (ast list -> ast)) list *
    1.12 +    (string * (term list -> term)) list *
    1.13 +    (string * (term list -> term)) list *
    1.14 +    (string * (ast list -> ast)) list -> sg -> sg
    1.15    val add_trfunsT:
    1.16 -    (bstring * (bool -> typ -> term list -> term)) list -> sg -> sg
    1.17 +    (string * (bool -> typ -> term list -> term)) list -> sg -> sg
    1.18    val add_tokentrfuns:
    1.19      (string * string * (string -> string * int)) list -> sg -> sg
    1.20    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg