src/HOL/Algebra/FiniteProduct.thy

--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -26,8 +26,7 @@
 
 inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
 
-constdefs
-  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
   "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
 
 lemma foldSetD_closed: