| changeset 8595 | 06874c5c3cfa |
| parent 8577 | 4a3cdf01531b |
| child 10572 | b070825579b8 |
--- 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 *)