| changeset 22798 | e3962371f568 |
| parent 22751 | 1bfd75c1f232 |
| child 23850 | f1434532a562 |
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Apr 26 13:32:55 2007 +0200 @@ -14,8 +14,8 @@ type 'a null = {null : 'a}; fun null (A_:'a null) = #null A_; -fun head A_ (x :: xs) = x - | head A_ [] = null A_; +fun head B_ (x :: xs) = x + | head B_ [] = null B_; val null_option : 'a option = NONE;