diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Aug 24 14:14:16 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Aug 24 14:14:17 2007 +0200
@@ -1,7 +1,7 @@
 structure Nat = 
 struct
 
-datatype nat = Zero_nat | Suc of nat;
+datatype nat = Suc of nat | Zero_nat;
 
 end; (*struct Nat*)
 
@@ -14,11 +14,9 @@
 fun head B_ (x :: xs) = x
   | head B_ [] = null B_;
 
-val null_option : 'a option = NONE;
-
-fun null_optiona () = {null = null_option} : ('b option) null;
+fun null_option () = {null = NONE} : ('b option) null;
 
 val dummy : Nat.nat option =
-  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
+  head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
 
 end; (*struct Codegen*)