--- 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,