diff -r 14c207135eff -r f22a564ac820 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Aug 23 12:13:58 2010 +0200
+++ b/src/HOL/Orderings.thy	Mon Aug 23 14:21:57 2010 +0200
@@ -1264,7 +1264,8 @@
 begin
 
 definition
-  top_fun_eq: "top = (\<lambda>x. top)"
+  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
+declare top_fun_eq_raw [no_atp]
 
 instance proof
 qed (simp add: top_fun_eq le_fun_def)