diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Fri Oct 12 08:20:43 2007 +0200
@@ -19,8 +19,11 @@
 fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;
 fun neutral (A_:'a monoidl) = #neutral A_;
 
-type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a};
-fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_;
+type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};
+fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;
+
+type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};
+fun monoid_group (A_:'a group) = #Classes__monoid_group A_;
 fun inverse (A_:'a group) = #inverse A_;
 
 fun inverse_int i = IntInf.~ i;
@@ -35,17 +38,21 @@
   {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :
   IntInf.int monoidl;
 
+val monoid_int = {Classes__monoidl_monoid = monoidl_int} :
+  IntInf.int monoid;
+
 val group_int =
-  {Classes__monoidl_group = monoidl_int, inverse = inverse_int} :
+  {Classes__monoid_group = monoid_int, inverse = inverse_int} :
   IntInf.int group;
 
-fun pow_nat B_ (Suc n) x =
-  mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x)
-  | pow_nat B_ Zero_nat x = neutral (monoidl_group B_);
+fun pow_nat A_ (Suc n) x =
+  mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x)
+  | pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_);
 
 fun pow_int A_ k x =
-  (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x
-    else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x));
+  (if IntInf.<= ((0 : IntInf.int), k)
+    then pow_nat (monoid_group A_) (nat k) x
+    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));
 
 val example : IntInf.int =
   pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);