# HG changeset patch
# User wenzelm
# Date 1005261503 -3600
# Node ID 7f8d88ed4f21cc5e352a4f1639976eb89ffbe1ce
# Parent  55b71be171c5bf21fa997f4fa749f3f8b7f0493f
indexvar_ast_tr (for \<index> placeholder);

diff -r 55b71be171c5 -r 7f8d88ed4f21 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Nov 09 00:17:52 2001 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Fri Nov 09 00:18:23 2001 +0100
@@ -161,6 +161,12 @@
   in (quoteN, tr) end;
 
 
+(* index variable *)
+
+fun indexvar_ast_tr [] = Ast.Variable "some_index"
+  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
+
+
 
 (** print (ast) translations **)
 
@@ -344,7 +350,8 @@
 
 val pure_trfuns =
  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
-   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
+   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
+   ("_indexvar", indexvar_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,