src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Jun 27 00:10:24 2015 +0200
@@ -167,7 +167,8 @@
     also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
     finally show ?thesis .
   next
-    show "A \<subseteq> F ==> ?thesis" by fact
+    show ?thesis when "A \<subseteq> F"
+      using that by fact
     assume "x \<notin> A"
     with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   qed