# HG changeset patch
# User wenzelm
# Date 902761434 -7200
# Node ID 0152d1a09639d41a9a48d0ef651c2e196a6edfb2
# Parent  0c055426fd6bd701fa601b15da71d5278b9fb8c3
tuned;

diff -r 0c055426fd6b -r 0152d1a09639 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Aug 10 17:01:40 1998 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Aug 10 17:03:54 1998 +0200
@@ -126,6 +126,12 @@
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
 
+(* binds *)
+
+fun bind_ast_tr (*"_BIND"*) [Variable x] = Variable (string_of_vname (binding x, 0))
+  | bind_ast_tr (*"_BIND"*) asts = raise AST ("bind_ast_tr", asts);
+
+
 (* quote / antiquote *)
 
 fun quote_antiquote_tr quoteN antiquoteN name =
@@ -326,7 +332,7 @@
 val pure_trfuns =
  ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
-   ("_bigimpl", bigimpl_ast_tr)],
+   ("_bigimpl", bigimpl_ast_tr), ("_BIND", bind_ast_tr)],
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    ("_TYPE", type_tr), ("_K", k_tr)],
   []: (string * (term list -> term)) list,