src/HOL/Smallcheck.thy
changeset 41178 f4d3acf0c4cc
parent 41177 810a885decee
child 41231 2e901158675e
     1.1 --- a/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
     1.2 +++ b/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
     1.3 @@ -281,7 +281,9 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option)) (t ())))"
     1.8 +  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
     1.9 +    (Code_Evaluation.Const (STR ''Option.option.Some'')
    1.10 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
    1.11  
    1.12  definition enum_term_of_option :: "'a option itself => unit => term list"
    1.13  where