1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Wed Apr 02 15:58:31 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Wed Apr 02 15:58:32 2008 +0200
     1.3 @@ -3,10 +3,10 @@
     1.4  
     1.5  datatype nat = Suc of nat | Zero_nat;
     1.6  
     1.7 -fun eqop_nat Zero_nat Zero_nat = true
     1.8 -  | eqop_nat (Suc m) (Suc n) = eqop_nat m n
     1.9 -  | eqop_nat Zero_nat (Suc a) = false
    1.10 -  | eqop_nat (Suc a) Zero_nat = false;
    1.11 +fun eq_nat Zero_nat Zero_nat = true
    1.12 +  | eq_nat (Suc m) (Suc n) = eq_nat m n
    1.13 +  | eq_nat Zero_nat (Suc a) = false
    1.14 +  | eq_nat (Suc a) Zero_nat = false;
    1.15  
    1.16  end; (*struct Nat*)
    1.17  
    1.18 @@ -27,8 +27,8 @@
    1.19  
    1.20  datatype monotype = Mono of Nat.nat * monotype list;
    1.21  
    1.22 -fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    1.23 -  Nat.eqop_nat tyco1 tyco2 andalso
    1.24 -    List.list_all2 eqop_monotype typargs1 typargs2;
    1.25 +fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    1.26 +  Nat.eq_nat tyco1 tyco2 andalso
    1.27 +    List.list_all2 eq_monotype typargs1 typargs2;
    1.28  
    1.29  end; (*struct Codegen*)