diff -r cc2be3315e72 -r 4ebe883b02ff 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];