diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -30,7 +30,7 @@
   random_seed :: "randseed \<Rightarrow> nat"
 
 definition
-  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed"
+  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
   "random n s = (random_seed s mod n, random_shift s)"
 
 lemma random_bound:
@@ -45,12 +45,13 @@
   "snd (random n s) = random_shift s" unfolding random_def by simp
 
 definition
-  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
   [simp]: "select xs = (do
       n \<leftarrow> random (length xs);
       return (nth xs n)
     done)"
-  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+definition
+  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
   [simp]: "select_weight xs = (do
       n \<leftarrow> random (foldl (op +) 0 (map fst xs));
       return (pick xs n)
@@ -123,7 +124,7 @@
 qed
 
 definition
-  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
+  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
   "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
 
 lemma random_nat [code]: