(* legacy ML bindings *) 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";