(* Simple insertion sort.  Paulson2, pp.109-110. *)
fun ins (x, []): real list = [x]
|   ins (x, y::ys) =
        if x <= y then x::y::ys (* x belongs here *)
                  else y::ins(x,ys);

(* Examples of use: ins(4.0, [6.0]); ins(8.0, it); ins(5.0, it) *)

fun insort [] = []
|   insort (x::xs) = ins(x, insort xs);

(* Example of use: insort([9.0, 7.0, 8.0, 3.0, 4.0, 2.0, 5.0]); *)