diff -r fc4d1ceb8e29 -r a0c985a57f7e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Jan 29 13:28:45 2017 +0100
+++ b/src/HOL/Power.thy	Sun Jan 29 13:43:17 2017 +0100
@@ -596,7 +596,7 @@
 
 lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
   by (induct n) (simp_all add: sgn_mult)
-    
+
 lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   by (simp add: power_abs)
 
@@ -842,18 +842,24 @@
 lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
 proof (induct rule: finite_induct)
   case empty
-  show ?case by auto
+  show ?case by simp
 next
   case (insert x A)
-  then have "inj_on (insert x) (Pow A)"
-    unfolding inj_on_def by (blast elim!: equalityE)
-  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
-    by (simp add: mult_2 card_image Pow_insert insert.hyps)
-  with insert show ?case
-    apply (simp add: Pow_insert)
-    apply (subst card_Un_disjoint)
-       apply auto
-    done
+  from \<open>x \<notin> A\<close> have disjoint: "Pow A \<inter> insert x ` Pow A = {}" by blast
+  from \<open>x \<notin> A\<close> have inj_on: "inj_on (insert x) (Pow A)"
+    unfolding inj_on_def by auto
+
+  have "card (Pow (insert x A)) = card (Pow A \<union> insert x ` Pow A)"
+    by (simp only: Pow_insert)
+  also have "\<dots> = card (Pow A) + card (insert x ` Pow A)"
+    by (rule card_Un_disjoint) (use \<open>finite A\<close> disjoint in simp_all)
+  also from inj_on have "card (insert x ` Pow A) = card (Pow A)"
+    by (rule card_image)
+  also have "\<dots> + \<dots> = 2 * \<dots>" by (simp add: mult_2)
+  also from insert(3) have "\<dots> = 2 ^ Suc (card A)" by simp
+  also from insert(1,2) have "Suc (card A) = card (insert x A)"
+    by (rule card_insert_disjoint [symmetric])
+  finally show ?case .
 qed