structure kozen2 = struct val thy = the_context () end ; val _ = use_legacy_bindings kozen2.thy ; structure KFun2 : KFUN = struct val idF = idF ; val compF = compF ; val idGo = idGo ; val idGa = idGa ; val compGo = compGo ; val compGa = compGa ; val ntGa_ty = ntGa_ty ; val theta_F_arr_def = theta_F_arr_def ; val theta_F_obj_arr_def = theta_F_obj_arr_def ; val etaG_F = etaG_F ; val thy = kozen2.thy ; end ; structure KT2 = KFunThms (KFun2) ; open KT2 ;