--- 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 *)