diff -r de0d280c31a7 -r 2c7a24f74db9 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:54:04 2009 +0200
@@ -36,7 +36,7 @@
 
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
-  [code inline]: "negateSnd = apsnd uminus"
+  [code_inline]: "negateSnd = apsnd uminus"
 
 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b