| changeset 42288 | 2074b31650e6 |
| parent 42284 | 326f57825e1a |
| child 42476 | d0bc1268ef09 |
--- a/src/Pure/Syntax/syntax_trans.ML Fri Apr 08 14:20:57 2011 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Apr 08 15:02:11 2011 +0200 @@ -185,7 +185,7 @@ (* dddot *) -fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts); +fun dddot_tr ts = Term.list_comb (Lexicon.var Syntax_Ext.dddot_indexname, ts); (* quote / antiquote *)