diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -2528,8 +2528,7 @@
   fold1Set_insertI [intro]:
    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
 
-constdefs
-  fold1 :: "('a => 'a => 'a) => 'a set => 'a"
+definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where
   "fold1 f A == THE x. fold1Set f A x"
 
 lemma fold1Set_nonempty: