1.1 --- a/src/HOL/Library/Random.thy	Fri Feb 06 09:05:19 2009 +0100
     1.2 +++ b/src/HOL/Library/Random.thy	Fri Feb 06 09:05:19 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Author:     Florian Haftmann, TU Muenchen
     1.5 -*)
     1.6 +(* Author: Florian Haftmann, TU Muenchen *)
     1.7  
     1.8  header {* A HOL random engine *}
     1.9  
    1.10 @@ -77,7 +76,7 @@
    1.11    in range_aux (k - 1) (v + l * 2147483561) s')"
    1.12  by pat_completeness auto
    1.13  termination
    1.14 -  by (relation "measure (nat_of_index o fst)")
    1.15 +  by (relation "measure (Code_Index.nat_of o fst)")
    1.16      (auto simp add: index)
    1.17  
    1.18  definition
    1.19 @@ -103,19 +102,19 @@
    1.20    select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
    1.21  where
    1.22    "select xs = (do
    1.23 -     k \<leftarrow> range (index_of_nat (length xs));
    1.24 -     return (nth xs (nat_of_index k))
    1.25 +     k \<leftarrow> range (Code_Index.of_nat (length xs));
    1.26 +     return (nth xs (Code_Index.nat_of k))
    1.27     done)"
    1.28  
    1.29  lemma select:
    1.30    assumes "xs \<noteq> []"
    1.31    shows "fst (select xs s) \<in> set xs"
    1.32  proof -
    1.33 -  from assms have "index_of_nat (length xs) > 0" by simp
    1.34 +  from assms have "Code_Index.of_nat (length xs) > 0" by simp
    1.35    with range have
    1.36 -    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
    1.37 +    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
    1.38    then have
    1.39 -    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
    1.40 +    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
    1.41    then show ?thesis
    1.42      by (auto simp add: monad_collapse select_def)
    1.43  qed