Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.
ToyList = Datatype +
datatype 'a list = Nil ("[]")
| Cons 'a ('a list) (infixr "#" 65)
consts app :: 'a list => 'a list => 'a list (infixr "@" 65)
rev :: 'a list => 'a list
primrec
"[] @ ys = ys"
"(x # xs) @ ys = x # (xs @ ys)"
primrec
"rev [] = []"
"rev (x # xs) = (rev xs) @ (x # [])"
end