renamed mapfilter to map_filter, made pervasive (again);
made flat pervasive (again);
added maps;
(* legacy ML bindings *)
val compact_ONE = thm "compact_ONE";
val dist_eq_one = thms "dist_eq_one";
val dist_less_one = thm "dist_less_one";
val Exh_one = thm "Exh_one";
val oneE = thm "oneE";