src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -1103,7 +1103,7 @@
 proof -
   from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
     by (auto dest: mk_disjoint_insert)
-  moreover from `finite A` this have "finite B" by simp
+  moreover from `finite A` A have "finite B" by simp
   ultimately show ?thesis by simp
 qed