diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -766,9 +766,8 @@
   assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
   shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" 
 proof -
-  have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
-  moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
-  ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
+  from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
+  with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
 qed
 
 lemma logical_subst_monotonicity :