diff -r c916828edc92 -r 5dbe537087aa src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Apr 02 20:19:38 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 03 10:15:43 2013 +0200
@@ -715,19 +715,52 @@
   then show ?thesis by simp
 qed
 
+end
+
 text{* Other properties of @{const fold}: *}
 
 lemma fold_image:
-  assumes "finite A" and "inj_on g A"
+  assumes "inj_on g A"
   shows "fold f z (g ` A) = fold (f \<circ> g) z A"
-using assms
-proof induction
-  case (insert a F)
-    interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute)
-    from insert show ?case by auto
-qed simp
-
-end
+proof (cases "finite A")
+  case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def)
+next
+  case True
+  have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
+  proof
+    fix w
+    show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
+    proof
+      assume ?P then show ?Q using assms
+      proof (induct "g ` A" w arbitrary: A)
+        case emptyI then show ?case by (auto intro: fold_graph.emptyI)
+      next
+        case (insertI x A r B)
+        from `inj_on g B` `x \<notin> A` `insert x A = image g B` obtain x' A' where
+          "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
+          by (rule inj_img_insertE)
+        from insertI.prems have "fold_graph (f o g) z A' r"
+          by (auto intro: insertI.hyps)
+        with `x' \<notin> A'` have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
+          by (rule fold_graph.insertI)
+        then show ?case by simp
+      qed
+    next
+      assume ?Q then show ?P using assms
+      proof induct
+        case emptyI thus ?case by (auto intro: fold_graph.emptyI)
+      next
+        case (insertI x A r)
+        from `x \<notin> A` insertI.prems have "g x \<notin> g ` A" by auto
+        moreover from insertI have "fold_graph f z (g ` A) r" by simp
+        ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
+          by (rule fold_graph.insertI)
+        then show ?case by simp
+      qed
+    qed
+  qed
+  with True assms show ?thesis by (auto simp add: fold_def)
+qed
 
 lemma fold_cong:
   assumes "comp_fun_commute f" "comp_fun_commute g"