1061     val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}

  1061     val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}

  1062     val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)

  1062     val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)

  1063     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver

  1063     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver

  1064   in

  1064   in

  1065     EVERY' [simp_tac (simps thms1),

  1065     EVERY' [simp_tac (simps thms1),

  1070             lambda_prs_tac lthy,

  1067             lambda_prs_tac lthy,

  1071             simp_tac (simps thms2),

  1068             simp_tac (simps thms2),

  1072             TRY o rtac refl]

  1069             TRY o rtac refl]

  1073   end

  1070   end

  1074 *}

  1071 *}