diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Divides.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -852,7 +852,7 @@
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
+interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
   proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
 
 lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"