--- a/IntEx.thy	Mon Oct 26 13:33:28 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 14:16:32 2009 +0100
@@ -114,26 +114,26 @@
   sorry
 
 lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
-  sorry
+  by (simp)
+
+ML {* val consts = [@{const_name "my_plus"}] *}
+ML {* val rty = @{typ "nat \<times> nat"} *}
+ML {* val qty = @{typ "my_int"} *}
+ML {* val rel = @{term "intrel"} *}
+ML {* val rel_eqv = @{thm equiv_intrel} *}
+ML {* val rel_refl = @{thm intrel_refl} *}
+ML {* val quot = @{thm QUOTIENT_my_int} *}
+ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *}
 
 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
-ML {* val t_r = regularize t_a @{typ "nat \<times> nat"} @{term "intrel"} @{thm equiv_intrel} @{context} *}
-ML {* val consts = [@{const_name "my_plus"}] *}
+ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
-ML {*
-  val rt = build_repabs_term @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}
-  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
-*}
-ML {*
-fun r_mk_comb_tac_myint ctxt =
-  r_mk_comb_tac ctxt @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}
-   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})
-*}
 ML {* val (g, thm, othm) =
   Toplevel.program (fn () =>
-  repabs_eq @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}
-   @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}
-   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})
+  repabs_eq @{context} t_r consts rty qty
+   quot rel_refl trans2
+   rsp_thms
   )
 *}
 ML {*
@@ -153,6 +153,30 @@
 done
 
 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_def}] ts
+  end
+*}
+
+
+
+ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
+thm HOL.sym[OF lambda_prs_mn_b,simplified]
+
+ML {*
   fun simp_lam_prs lthy thm =
     simp_lam_prs lthy (eqsubst_thm lthy
       @{thms HOL.sym[OF lambda_prs_mn_b,simplified]}
@@ -161,7 +185,7 @@
 *}
 ML {* t_t2 *}
 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
-ML {* findabs @{typ "nat \<times> nat"} (prop_of (atomize_thm @{thm plus_sym_pre})) *}
+ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 
 ML {*
   fun simp_allex_prs lthy thm =