--- a/IntEx.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -246,18 +246,11 @@
 
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-defer
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(simp only: prod_rel.simps)
+(*apply(tactic {* regularize_tac @{context} 1 *}) *)
 defer
-apply(tactic {* clean_tac @{context} 1 *})
-apply(simp add: prod_rel.simps)
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp)
-(*apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})*)
+apply(simp add: prod_fun_def) (* Should be pair_prs *)
 sorry
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"