--- a/IntEx.thy	Mon Dec 07 08:45:04 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 11:14:21 2009 +0100
@@ -250,7 +250,7 @@
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp add: prod_fun_def) (* Should be pair_prs *)
+apply(simp add: pair_prs)
 sorry
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
@@ -259,6 +259,9 @@
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 apply(tactic {* gen_frees_tac @{context} 1 *})
+ML_prf {* regularize_trm @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
+ML_prf {* print_depth 50 *}
+ML_prf {* Syntax.check_term @{context} it *}
 ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
 
 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})