diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -55,15 +55,19 @@
 qed
 
 definition (in ordered)
-  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "min x y = (if x \<^loc><<= y then x else y)"
-  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+definition (in ordered)
+  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max x y = (if x \<^loc><<= y then y else x)"
 
 definition
-  min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+  min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where
   "min x y = (if x <<= y then x else y)"
-  max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+
+definition
+  max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max x y = (if x <<= y then y else x)"
 
 fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -366,15 +370,15 @@
   "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"
 
 definition
-  between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option"
+  between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where
   "between x y = get_first (\<lambda>z. x << z & z << y) enum"
 
 definition
-  index :: "'a::enum \<Rightarrow> nat"
+  index :: "'a::enum \<Rightarrow> nat" where
   "index x = the (get_index (\<lambda>y. y = x) 0 enum)"
 
 definition
-  add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a"
+  add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where
   "add x y =
     (let
       enm = enum
@@ -387,9 +391,8 @@
   "sum [] = inf"
   "sum (x#xs) = add x (sum xs)"
 
-definition
-  "test1 = sum [None, Some True, None, Some False]"
-  "test2 = (inf :: nat \<times> unit)"
+definition "test1 = sum [None, Some True, None, Some False]"
+definition "test2 = (inf :: nat \<times> unit)"
 
 code_gen "op <<="
 code_gen "op <<"