1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 10 17:48:17 2014 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 10 17:48:18 2014 +0200
     1.3 @@ -2508,7 +2508,7 @@
     1.4  lemma bi_total_rel_filter [transfer_rule]:
     1.5    assumes "bi_total A" "bi_unique A"
     1.6    shows "bi_total (rel_filter A)"
     1.7 -unfolding bi_total_conv_left_right using assms
     1.8 +unfolding bi_total_alt_def using assms
     1.9  by(simp add: left_total_rel_filter right_total_rel_filter)
    1.10  
    1.11  lemma left_unique_rel_filter [transfer_rule]:
    1.12 @@ -2535,7 +2535,7 @@
    1.13  
    1.14  lemma bi_unique_rel_filter [transfer_rule]:
    1.15    "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
    1.16 -by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter)
    1.17 +by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
    1.18  
    1.19  lemma top_filter_parametric [transfer_rule]:
    1.20    "bi_total A \<Longrightarrow> (rel_filter A) top top"