# HG changeset patch
# User blanchet
# Date 1286379486 -7200
# Node ID 03174b2d075c09ef95582cd7863d50e43893dbff
# Parent  12eb8fe15b004806632a70d5cf94835bab9c742d
remove needless fact

diff -r 12eb8fe15b00 -r 03174b2d075c src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 06 12:01:55 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 06 17:38:06 2010 +0200
@@ -242,7 +242,7 @@
 lemma sigma_sets_Un:
   "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
 apply (simp add: Un_range_binary range_binary_eq)
-apply (rule Union, simp add: binary_def COMBK_def fun_upd_apply)
+apply (rule Union, simp add: binary_def fun_upd_apply)
 done
 
 lemma sigma_sets_Inter: