token translations: context dependent, result Pretty.T;
authorwenzelm
Thu Apr 17 16:30:47 2008 +0200 (2008-04-17)
changeset 26701341c4d51d1c2
parent 26700 493db7848904
child 26702 a079f8f0080b
token translations: context dependent, result Pretty.T;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Apr 17 16:30:45 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 17 16:30:47 2008 +0200
     1.3 @@ -135,8 +135,8 @@
     1.4    val add_advanced_trfunsT:
     1.5      (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
     1.6    val add_tokentrfuns:
     1.7 -    (string * string * (string -> output * int)) list -> theory -> theory
     1.8 -  val add_mode_tokentrfuns: string -> (string * (string -> output * int)) list
     1.9 +    (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
    1.10 +  val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
    1.11      -> theory -> theory
    1.12    val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    1.13    val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory