src/Pure/Syntax/syn_trans.ML
changeset 28856 5e009a80fe6d
parent 28628 06737d425249
child 29276 94b1ffec9201
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -473,9 +473,8 @@
     1.4     ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
     1.5     ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
     1.6    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
     1.7 -   ("_sort_constraint", sort_constraint_tr), ("\\<^fixed>meta_conjunction", conjunction_tr),
     1.8 -   ("_TYPE", type_tr), ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr),
     1.9 -   ("_index", index_tr)],
    1.10 +   ("_sort_constraint", sort_constraint_tr), ("_TYPE", type_tr),
    1.11 +   ("_DDDOT", dddot_tr), ("_index", index_tr)],
    1.12    ([]: (string * (term list -> term)) list),
    1.13    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    1.14     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),