diff -r f0aeca99b5d9 -r 461ee3e49ad3 doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -458,7 +458,7 @@
   of monoids for lists:
 *}
 
-interpretation %quote list_monoid!: monoid append "[]"
+interpretation %quote list_monoid: monoid append "[]"
   proof qed auto
 
 text {*
@@ -473,7 +473,7 @@
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-interpretation %quote list_monoid!: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" where
   "monoid.pow_nat append [] = replicate"
 proof -
   interpret monoid append "[]" ..