854 ML {*

   855 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let

   856   val t_a = atomize_thm t;

   857   val t_r = regularize t_a rty rel rel_eqv lthy;

   858   val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;

   859   val t_t2 = repabs_eq2 lthy t_t1;

   860   val abs = findabs rty (prop_of t_a);

   861   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;

   862   fun simp_lam_prs lthy thm =

   863     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)

   864     handle _ => thm

   865   val t_l = simp_lam_prs lthy t_t2;

   866   val t_a = simp_allex_prs lthy quot t_l;

   867   val t_defs_sym = add_lower_defs lthy t_defs;

   868   val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;

   869   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

   870 in

   871   ObjectLogic.rulify t_r

   873 *}

   874 

   875 end