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