diff -r fa8a7de5da28 -r 03fe6d36e948 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Dec 02 02:52:07 2006 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Dec 02 11:33:08 2006 +0100
@@ -428,7 +428,7 @@
 *}
 
 consts
-  foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
+  foldSet :: "('a => 'b => 'b) => ('c => 'a) => 'b => ('c set \<times> 'b) set"
 
 inductive "foldSet f g z"
 intros
@@ -440,7 +440,7 @@
 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
 
 constdefs
-  fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
+  fold :: "('a => 'b => 'b) => ('c => 'a) => 'b => 'c set => 'b"
   "fold f g z A == THE x. (A, x) : foldSet f g z"
 
 text{*A tempting alternative for the definiens is