# HG changeset patch
# User wenzelm
# Date 1208442647 -7200
# Node ID 341c4d51d1c215753945304f10c501237a991cb7
# Parent  493db7848904c4697ca29c798b2125aa292359bb
token translations: context dependent, result Pretty.T;

diff -r 493db7848904 -r 341c4d51d1c2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 17 16:30:45 2008 +0200
+++ b/src/Pure/sign.ML	Thu Apr 17 16:30:47 2008 +0200
@@ -135,8 +135,8 @@
   val add_advanced_trfunsT:
     (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
-    (string * string * (string -> output * int)) list -> theory -> theory
-  val add_mode_tokentrfuns: string -> (string * (string -> output * int)) list
+    (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
+  val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
     -> theory -> theory
   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory