--- a/src/HOL/Random.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Random.thy Tue Sep 07 10:05:19 2010 +0200
@@ -85,7 +85,7 @@
lemma pick_drop_zero:
"pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
- by (induct xs) (auto simp add: expand_fun_eq)
+ by (induct xs) (auto simp add: ext_iff)
lemma pick_same:
"l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
@@ -132,7 +132,7 @@
by (induct xs) simp_all
ultimately show ?thesis
by (auto simp add: select_weight_def select_def scomp_def split_def
- expand_fun_eq pick_same [symmetric])
+ ext_iff pick_same [symmetric])
qed