# HG changeset patch
# User wenzelm
# Date 936471870 -7200
# Node ID fd03510c6841b3bf72914eabd54b7c57d9e47cda
# Parent  f1208505d83779c23ed10c5c972212e0d70e6225
removed "_BIND" translation;

diff -r f1208505d837 -r fd03510c6841 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sat Sep 04 21:04:07 1999 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Sep 04 21:04:30 1999 +0200
@@ -125,13 +125,6 @@
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
 
-(* binds *)
-
-fun bind_ast_tr (*"_BIND"*) [Ast.Variable x] =
-      Ast.Variable (Lexicon.string_of_vname (Lexicon.binding x, 0))
-  | bind_ast_tr (*"_BIND"*) asts = raise Ast.AST ("bind_ast_tr", asts);
-
-
 (* dddot *)
 
 fun dddot_tr (*"_DDDOT"*) [] = Lexicon.var SynExt.dddot_indexname
@@ -335,7 +328,7 @@
 val pure_trfuns =
  ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
-   ("_bigimpl", bigimpl_ast_tr), ("_BIND", bind_ast_tr)],
+   ("_bigimpl", bigimpl_ast_tr)],
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   []: (string * (term list -> term)) list,