1.1 --- a/src/HOL/Orderings.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Orderings.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -1309,10 +1309,10 @@
     1.4  
     1.5  instance "fun" :: (type, preorder) preorder proof
     1.6  qed (auto simp add: le_fun_def less_fun_def
     1.7 -  intro: order_trans antisym intro!: ext)
     1.8 +  intro: order_trans antisym)
     1.9  
    1.10  instance "fun" :: (type, order) order proof
    1.11 -qed (auto simp add: le_fun_def intro: antisym ext)
    1.12 +qed (auto simp add: le_fun_def intro: antisym)
    1.13  
    1.14  instantiation "fun" :: (type, bot) bot
    1.15  begin