theory FrogList imports Main begin ML {* datatype nat = zero | suc of nat; fun frogs (zero) = "" | frogs (suc(n)) = "frog " ^ frogs n; datatype 'a List = NIL | CONS of ('a * 'a List); fun mapfrogs (NIL) = NIL | mapfrogs (CONS (a,x)) = CONS (frogs a, mapfrogs x); val one = suc zero; val two = suc one; val three = suc two; val numlist = CONS (one, CONS(two, CONS(three, NIL))); val froglist = mapfrogs numlist; *} end