(* legacy ML bindings *) val Exh_one = thm "Exh_one"; val oneE = thm "oneE"; val dist_less_one = thm "dist_less_one"; val dist_eq_one = thms "dist_eq_one";