src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Sun Feb 05 08:24:39 2012 +0100
+++ b/src/HOL/Fun.thy	Sun Feb 05 08:36:41 2012 +0100
@@ -427,6 +427,7 @@
   using * by blast
 qed
 
+(* FIXME: bij_betw_Disj_Un is special case of bij_betw_combine -- should be removed *)
 lemma bij_betw_Disj_Un:
   assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
           B1: "bij_betw f A A'" and B2: "bij_betw f B B'"