structure kozen1 = struct val thy = the_context () end ; val _ = use_legacy_bindings kozen1.thy ; structure KFun1 : 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 = kozen1.thy ; end ; structure KT1 = KFunThms (KFun1) ; open KT1 ;