# HG changeset patch
# User urbanc
# Date 1133694880 -3600
# Node ID c9be8266325f01971242de20b5d1f39fa86fe0e2
# Parent  d37fb71754fe4ca2be4712d366a6b8fea5b916d2
tuned

diff -r d37fb71754fe -r c9be8266325f src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sun Dec 04 12:14:27 2005 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Sun Dec 04 12:14:40 2005 +0100
@@ -215,7 +215,7 @@
   have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp 
   moreover
   have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force
-  ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force
+  ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp 
   with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force
 qed (auto simp add: sub_def) (* app and var case *)