1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Nov 09 00:17:52 2001 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Nov 09 00:18:23 2001 +0100
     1.3 @@ -161,6 +161,12 @@
     1.4    in (quoteN, tr) end;
     1.5  
     1.6  
     1.7 +(* index variable *)
     1.8 +
     1.9 +fun indexvar_ast_tr [] = Ast.Variable "some_index"
    1.10 +  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
    1.11 +
    1.12 +
    1.13  
    1.14  (** print (ast) translations **)
    1.15  
    1.16 @@ -344,7 +350,8 @@
    1.17  
    1.18  val pure_trfuns =
    1.19   ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
    1.20 -   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
    1.21 +   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
    1.22 +   ("_indexvar", indexvar_ast_tr)],
    1.23    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    1.24     ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
    1.25    []: (string * (term list -> term)) list,