src/HOL/Smallcheck.thy
changeset 41178 f4d3acf0c4cc
parent 41177 810a885decee
child 41231 2e901158675e
--- a/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
@@ -281,7 +281,9 @@
 begin
 
 definition
-  "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 ())))"
+  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
+    (Code_Evaluation.Const (STR ''Option.option.Some'')
+      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
 
 definition enum_term_of_option :: "'a option itself => unit => term list"
 where