# HG changeset patch
# User wenzelm
# Date 1169240900 -3600
# Node ID b3f5b654bcd342f56180688243eda0c8e1af4f22
# Parent  f9eb6328bdbdadf4576dfd5ddd72772b1416231c
moved ML translation interfaces to isar_cmd.ML;

diff -r f9eb6328bdbd -r b3f5b654bcd3 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jan 19 22:08:19 2007 +0100
+++ b/src/Pure/sign.ML	Fri Jan 19 22:08:20 2007 +0100
@@ -46,12 +46,6 @@
     (string * string * (string -> string * real)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
     -> theory -> theory
-  val parse_ast_translation: bool * string -> theory -> theory
-  val parse_translation: bool * string -> theory -> theory
-  val print_translation: bool * string -> theory -> theory
-  val typed_print_translation: bool * string -> theory -> theory
-  val print_ast_translation: bool * string -> theory -> theory
-  val token_translation: string -> theory -> theory
   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
@@ -825,56 +819,6 @@
 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
 
 
-(* compile translation functions *)
-
-local
-
-fun advancedT false = ""
-  | advancedT true = "Proof.context -> ";
-
-fun advancedN false = ""
-  | advancedN true = "advanced_";
-
-in
-
-fun parse_ast_translation (a, txt) =
-  txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
-    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
-  |> Context.theory_map;
-
-fun parse_translation (a, txt) =
-  txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
-      "term list -> term)) list")
-    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
-  |> Context.theory_map;
-
-fun print_translation (a, txt) =
-  txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
-      "term list -> term)) list")
-    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
-  |> Context.theory_map;
-
-fun print_ast_translation (a, txt) =
-  txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
-    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
-  |> Context.theory_map;
-
-fun typed_print_translation (a, txt) =
-  txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
-      "bool -> typ -> term list -> term)) list")
-    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
-  |> Context.theory_map;
-
-val token_translation =
-  Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
-    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
-  #> Context.theory_map;
-
-end;
-
-
 (* translation rules *)
 
 fun gen_trrules f args thy = thy |> map_syn (fn syn =>