src/HOL/Finite_Set.thy

   for f :: "'a => 'a => 'a"
 where
   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:
   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
 by(erule fold1Set.cases, simp_all)