# HG changeset patch
# User wenzelm
# Date 954184386 -7200
# Node ID 06874c5c3cfa5abaeaa019ae3f374f2cf26f85f0
# Parent  d2e2a3df6871c6e8040b2e62306854b7e49c5538
fixed dddot_tr;

diff -r d2e2a3df6871 -r 06874c5c3cfa src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Mar 27 18:10:11 2000 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Mar 27 21:13:06 2000 +0200
@@ -131,8 +131,7 @@
 
 (* dddot *)
 
-fun dddot_tr (*"_DDDOT"*) [] = Lexicon.var SynExt.dddot_indexname
-  | dddot_tr (*"_DDDOT"*) ts = raise TERM ("dddot_tr", ts);
+fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);
 
 
 (* quote / antiquote *)