src/HOL/Library/Code_Target_Int.thy

--- a/src/HOL/Library/Code_Target_Int.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -103,7 +103,7 @@
   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   show ?thesis
     by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
-      (simp add: * mult_commute)
+      (simp add: * mult.commute)
 qed
 
 declare of_int_code_if [code]