1.1 --- a/src/HOL/ex/FinFunPred.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/ex/FinFunPred.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  instance "finfun" :: (type, order) order
     1.5  by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
     1.6  
     1.7 -instantiation "finfun" :: (type, bot) bot begin
     1.8 +instantiation "finfun" :: (type, order_bot) order_bot begin
     1.9  definition "bot = finfun_const bot"
    1.10  instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
    1.11  end
    1.12 @@ -39,7 +39,7 @@
    1.13  lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
    1.14  by(auto simp add: bot_finfun_def)
    1.15  
    1.16 -instantiation "finfun" :: (type, top) top begin
    1.17 +instantiation "finfun" :: (type, order_top) order_top begin
    1.18  definition "top = finfun_const top"
    1.19  instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
    1.20  end