diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -307,8 +307,8 @@
 
 subsection {* Least value operator *}
 
-constdefs
-  LeastM :: "['a => 'b::ord, 'a => bool] => 'a"
+definition
+  LeastM :: "['a => 'b::ord, 'a => bool] => 'a" where
   "LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
 
 syntax
@@ -360,11 +360,12 @@
 
 subsection {* Greatest value operator *}
 
-constdefs
-  GreatestM :: "['a => 'b::ord, 'a => bool] => 'a"
+definition
+  GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" where
   "GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
 
-  Greatest :: "('a::ord => bool) => 'a"    (binder "GREATEST " 10)
+definition
+  Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) where
   "Greatest == GreatestM (%x. x)"
 
 syntax