diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -1033,9 +1033,9 @@
   case (insert x A)
   from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
     by (auto simp add: in_fset)
-  then have "A = B - {|x|}" by (rule insert.hyps(2))
-  moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
-  ultimately show ?case by (metis in_fset_mdef)
+  then have A: "A = B - {|x|}" by (rule insert.hyps(2))
+  with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
+  with A show ?case by (metis in_fset_mdef)
 qed
 
 subsection {* alternate formulation with a different decomposition principle