src/HOL/Tools/smallvalue_generators.ML
changeset 40899 ef6fde932f4c
parent 40845 15b97bd4b5c0
child 40901 8fdfa9c4e7ed
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     1.3 @@ -50,8 +50,8 @@
     1.4    let
     1.5      val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
     1.6    in
     1.7 -    Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
     1.8 -      $ y $ Const (@{const_name Some}, T' --> T) $ x
     1.9 +    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
    1.10 +      $ x $ y
    1.11    end
    1.12  
    1.13  (** datatypes **)