(* 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";