1.1 --- a/src/HOL/Orderings.thy	Sat Mar 17 00:17:30 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sat Mar 17 09:51:18 2012 +0100
     1.3 @@ -1314,7 +1314,6 @@
     1.4  
     1.5  definition
     1.6    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
     1.7 -declare top_fun_def_raw [no_atp]
     1.8  
     1.9  lemma top_apply [simp] (* CANDIDATE [code] *):
    1.10    "\<top> x = \<top>"