--- a/IntEx.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 15:31:53 2009 +0100
@@ -142,15 +142,6 @@
     repabs_eq2 @{context} (g, thm, othm)
   )
 *}
-ML {*
- val lpi = Drule.instantiate'
-   [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
-*}
-prove lambda_prs_mn_b : {* concl_of lpi *}
-apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-done
 
 ML {*
 fun make_simp_lam_prs_thm lthy quot_thm typ =
@@ -166,26 +157,23 @@
     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
+    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
   end
 *}
 
 
-
+thm id_apply
 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]}
-    thm)
+    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
 ML {* t_t2 *}
 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
-ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 
 ML {*
   fun simp_allex_prs lthy thm =