doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 23850 f1434532a562
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:11:09 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:17:48 2007 +0100
     1.3 @@ -6,7 +6,8 @@
     1.4  
     1.5  val arbitrary_option : 'a option = NONE;
     1.6  
     1.7 -fun dummy_option [] = arbitrary_option;
     1.8 +fun dummy_option [] = arbitrary_option
     1.9 +  | dummy_option (x :: xs) = SOME x;
    1.10  
    1.11  end; (*struct Codegen*)
    1.12