diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Aug 24 14:14:16 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Aug 24 14:14:17 2007 +0200
@@ -1,12 +1,12 @@
 structure Nat = 
 struct
 
-datatype nat = Zero_nat | Suc of nat;
+datatype nat = Suc of nat | Zero_nat;
 
-fun eq_nat Zero_nat (Suc m) = false
-  | eq_nat (Suc n) Zero_nat = false
-  | eq_nat (Suc n) (Suc m) = eq_nat n m
-  | eq_nat Zero_nat Zero_nat = true;
+fun eqop_nat Zero_nat (Suc m) = false
+  | eqop_nat (Suc n) Zero_nat = false
+  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
+  | eqop_nat Zero_nat Zero_nat = true;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat n = n;
@@ -39,7 +39,7 @@
   | list_all2 p xs [] = null xs
   | list_all2 p [] ys = null ys
   | list_all2 p xs ys =
-    Nat.eq_nat (size_list xs) (size_list ys) andalso
+    Nat.eqop_nat (size_list xs) (size_list ys) andalso
       list_all (fn a as (aa, b) => p aa b) (zip xs ys);
 
 end; (*struct List*)
@@ -49,8 +49,8 @@
 
 datatype monotype = Mono of Nat.nat * monotype list;
 
-fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
-  Nat.eq_nat tyco1 tyco2 andalso
-    List.list_all2 eq_monotype typargs1 typargs2;
+fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
+  Nat.eqop_nat tyco1 tyco2 andalso
+    List.list_all2 eqop_monotype typargs1 typargs2;
 
 end; (*struct Codegen*)