| changeset 21994 | dfa5133dbe73 |
| parent 21993 | 4b802a9e0738 |
| child 22188 | a63889770d57 |
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 17:11:09 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 17:17:48 2007 +0100 @@ -14,7 +14,8 @@ type 'a null = {null_ : 'a}; fun null (A_:'a null) = #null_ A_; -fun head (A_:'a null) (y :: xs) = y; +fun head (A_:'a null) (y :: xs) = y + | head (A_:'a null) [] = null A_; val null_option : 'b option = NONE;