diff -r 0a451e1e6176 -r 00b7b55b61bd doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sat Jun 14 15:58:36 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Jun 14 17:26:07 2008 +0200
@@ -1262,16 +1262,12 @@
     @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
     @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
     @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
-    @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
   \begin{rail}
   ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
     'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
   ;
-
-  'token\_translation' text
-  ;
   \end{rail}
 
   Syntax translation functions written in ML admit almost arbitrary
@@ -1287,8 +1283,6 @@
 val typed_print_translation :
   (string * (bool -> typ -> term list -> term)) list
 val print_ast_translation   : (string * (ast list -> ast)) list
-val token_translation       :
-  (string * string * (string -> string * real)) list
 \end{ttbox}
 
   If the @{text "(advanced)"} option is given, the corresponding