--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Oct 16 17:07:40 2007 +0200
@@ -14,9 +14,11 @@
fun head B_ (x :: xs) = x
| head B_ [] = null B_;
-fun null_option () = {null = NONE} : ('a option) null;
+val null_option : 'a option = NONE;
+
+fun null_optiona () = {null = null_option} : ('a option) null;
val dummy : Nat.nat option =
- head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
+ head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
end; (*struct Codegen*)