diff -r f12613fda79d -r 5200374fda5d doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Nov 09 23:24:31 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Sat Nov 10 14:31:18 2007 +0100
@@ -412,7 +412,7 @@
   a canonical interpretation as type classes.
   Anyway, there is also the possibility of other interpretations.
   For example, also @{text "list"}s form a monoid with
-  @{const "op @"} and @{const "[]"} as operations, but it
+  @{term "op @"} and @{term "[]"} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinly algebraic types.
   In such a case, we simply can do a particular interpretation