--- a/QuotMain.thy	Mon Oct 26 19:35:30 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 07:46:52 2009 +0100
@@ -820,4 +820,35 @@
     | _ => []
 *}
 
+ML {*
+fun make_simp_lam_prs_thm lthy quot_thm typ =
+  let
+    val (_, [lty, rty]) = dest_Type typ;
+    val thy = ProofContext.theory_of lthy;
+    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+    val inst = [SOME lcty, NONE, SOME rcty];
+    val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};
+    val tac =
+      (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW
+      (quotient_tac quot_thm);
+    val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
+    val ts = @{thm HOL.sym} OF [t]
+  in
+    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
+  end
+*}
+
+ML {*
+  fun simp_allex_prs lthy quot thm =
+    let
+      val rwf = @{thm FORALL_PRS} OF [quot];
+      val rwfs = @{thm "HOL.sym"} OF [rwf];
+      val rwe = @{thm EXISTS_PRS} OF [quot];
+      val rwes = @{thm "HOL.sym"} OF [rwe]
+    in
+      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
+    end
+    handle _ => thm
+*}
+
 end