1 Sep2 = Main +
2 consts sep :: 'a list => 'a => 'a list
3 recdef sep "measure length"
4 "sep (x#y#zs) = (%a. x # a # sep zs a)"
5 "sep xs = (%a. xs)"
6 end