1.1 --- a/src/HOL/Library/Old_Recdef.thy	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    less_Suc_eq [THEN iffD2]
     1.5  
     1.6  lemmas [recdef_cong] =
     1.7 -  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
     1.8 +  if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
     1.9    map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
    1.10  
    1.11  lemmas [recdef_wf] =