crude adaption to intermediate class/locale version;

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Jan 01 20:56:23 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Jan 01 21:00:33 2009 +0100
@@ -375,8 +375,8 @@
 
 text {* \noindent together with a corresponding interpretation: *}
 
-interpretation %quote idem_class:
-  idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
+interpretation %quote idem_class':    (* FIXME proper prefix? *)
+  idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
 proof qed (rule idem)
 
 text {*
@@ -459,7 +459,7 @@
   of monoids for lists:
 *}
 
-interpretation %quote list_monoid: monoid [append "[]"]
+class_interpretation %quote list_monoid: monoid [append "[]"]
   proof qed auto
 
 text {*
@@ -474,10 +474,10 @@
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-interpretation %quote list_monoid: monoid [append "[]"] where
+class_interpretation %quote list_monoid: monoid [append "[]"] where
   "monoid.pow_nat append [] = replicate"
 proof -
-  interpret monoid [append "[]"] ..
+  class_interpret monoid [append "[]"] ..
   show "monoid.pow_nat append [] = replicate"
   proof
     fix n