(* legacy ML bindings *)
val less_sprod_def = thm "less_sprod_def";
val spair_def = thm "spair_def";
val sfst_def = thm "sfst_def";
val ssnd_def = thm "ssnd_def";
val ssplit_def = thm "ssplit_def";
val inject_spair = thm "inject_spair";
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
val strict_spair = thm "strict_spair";
val strict_spair1 = thm "strict_spair1";
val strict_spair2 = thm "strict_spair2";
val strict_spair_rev = thm "strict_spair_rev";
val defined_spair_rev = thm "defined_spair_rev";
val defined_spair = thm "defined_spair";
val Exh_Sprod2 = thm "Exh_Sprod2";
val sprodE = thm "sprodE";
val strict_sfst = thm "strict_sfst";
val strict_ssnd = thm "strict_ssnd";
val sfst2 = thm "sfst2";
val ssnd2 = thm "ssnd2";
val defined_sfstssnd = thm "defined_sfstssnd";
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
val ssplit1 = thm "ssplit1";
val ssplit2 = thm "ssplit2";
val ssplit3 = thm "ssplit3";