diff -r 25472dc71a4b -r 363f17dee9ca doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Jan 16 14:59:06 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Jan 16 15:14:16 2009 +0100
@@ -368,14 +368,14 @@
 text {*
   \noindent The connection to the type system is done by means
   of a primitive axclass
-*}
+*} setup %invisible {* Sign.add_path "foo" *}
 
 axclass %quote idem < type
-  idem: "f (f x) = f x"
+  idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
 
 text {* \noindent together with a corresponding interpretation: *}
 
-interpretation %quote idem_class':    (* FIXME proper prefix? *)
+interpretation %quote idem_class:
   idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
 proof qed (rule idem)
 
@@ -459,7 +459,7 @@
   of monoids for lists:
 *}
 
-class_interpretation %quote list_monoid: monoid [append "[]"]
+interpretation %quote list_monoid!: monoid append "[]"
   proof qed auto
 
 text {*
@@ -474,10 +474,10 @@
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-class_interpretation %quote list_monoid: monoid [append "[]"] where
+interpretation %quote list_monoid!: monoid append "[]" where
   "monoid.pow_nat append [] = replicate"
 proof -
-  class_interpret monoid [append "[]"] ..
+  interpret monoid append "[]" ..
   show "monoid.pow_nat append [] = replicate"
   proof
     fix n