# HG changeset patch
# User wenzelm
# Date 1213457167 -7200
# Node ID 00b7b55b61bd7d500cccc5bca24143af2194f345
# Parent  0a451e1e61769aed6fc1270ea8381434c1093c72
removed exotic 'token_translation' command;

diff -r 0a451e1e6176 -r 00b7b55b61bd NEWS
--- a/NEWS	Sat Jun 14 15:58:36 2008 +0200
+++ b/NEWS	Sat Jun 14 17:26:07 2008 +0200
@@ -15,6 +15,9 @@
 
 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
 
+* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
+interface instead.
+
 
 *** HOL ***
 
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
diff -r 0a451e1e6176 -r 00b7b55b61bd src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Jun 14 15:58:36 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jun 14 17:26:07 2008 +0200
@@ -13,7 +13,6 @@
   val print_translation: bool * (string * Position.T) -> theory -> theory
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val token_translation: string * Position.T -> theory -> theory
   val oracle: bstring -> string -> string * Position.T -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
@@ -184,12 +183,6 @@
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   |> Context.theory_map;
 
-fun token_translation (txt, pos) =
-  txt |> ML_Context.expression pos
-    "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list"
-      "Context.map_theory (Sign.add_tokentrfuns token_translation)"
-  |> Context.theory_map;
-
 end;
 
 
diff -r 0a451e1e6176 -r 00b7b55b61bd src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jun 14 15:58:36 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 14 17:26:07 2008 +0200
@@ -361,11 +361,6 @@
     (K.tag_ml K.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
 
-val _ =
-  OuterSyntax.command "token_translation" "install token translation functions"
-    (K.tag_ml K.thy_decl)
-    (P.position P.text >> (Toplevel.theory o IsarCmd.token_translation));
-
 
 (* oracles *)