# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260180861 -3600
# Node ID 6346745532f4a0a9c1b8b699ab089e7f754b295b
# Parent  18eac4596ef1c155586b54d3a49470a192944c86
Using pair_prs; debugging the error in regularize of a lambda.

diff -r 18eac4596ef1 -r 6346745532f4 IntEx.thy
--- 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 *})