diff -r f737a88a3248 -r 0fcb4775cbfb src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Oct 24 07:19:52 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Oct 24 07:19:53 2007 +0200
@@ -384,7 +384,7 @@
 definition
   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
 where
-  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
+  "neg Z \<longleftrightarrow> Z < 0"
 
 definition (*for simplifying equalities*)
   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"