doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -11,15 +11,15 @@
 structure Codegen = 
 struct
 
-type 'a null = {Codegen__null : 'a};
-fun null (A_:'a null) = #Codegen__null A_;
+type 'a null = {null : 'a};
+fun null (A_:'a null) = #null A_;
 
 fun head A_ (y :: xs) = y
   | head A_ [] = null A_;
 
 val null_option : 'a option = NONE;
 
-fun null_optiona () = {Codegen__null = null_option} : ('b option) null;
+fun null_optiona () = {null = null_option} : ('b option) null;
 
 val dummy : Nat.nat option =
   head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];