823 ML {*

   824 fun make_simp_lam_prs_thm lthy quot_thm typ =

   825   let

   826     val (_, [lty, rty]) = dest_Type typ;

   827     val thy = ProofContext.theory_of lthy;

   828     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)

   829     val inst = [SOME lcty, NONE, SOME rcty];

   830     val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};

   831     val tac =

   832       (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW

   833       (quotient_tac quot_thm);

   834     val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);

   835     val ts = @{thm HOL.sym} OF [t]

   836   in

   837     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts

   838   end

   839 *}

   840 

   841 ML {*

   842   fun simp_allex_prs lthy quot thm =

   843     let

   844       val rwf = @{thm FORALL_PRS} OF [quot];

   845       val rwfs = @{thm "HOL.sym"} OF [rwf];

   846       val rwe = @{thm EXISTS_PRS} OF [quot];

   847       val rwes = @{thm "HOL.sym"} OF [rwe]

   848     in

   849       (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))

   850     end

   851     handle _ => thm

   852 *}

   853