# HG changeset patch
# User wenzelm
# Date 1140698266 -3600
# Node ID 06b6f5f8e4cb27e223bfc1ecb64b41929770ba4e
# Parent  b23479b808288ab5f0630761368ba4f4039da19c
make SML/NJ happy;

diff -r b23479b80828 -r 06b6f5f8e4cb src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Thu Feb 23 13:00:18 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Feb 23 13:37:46 2006 +0100
@@ -438,7 +438,7 @@
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    ("_TYPE", type_tr), ("_DDDOT", dddot_tr),
    ("_index", index_tr)],
-  [],
+  ([]: (string * (term list -> term)) list),
   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
    ("_index", index_ast_tr')]);