# HG changeset patch
# User haftmann
# Date 1247205565 -7200
# Node ID a6e982b1ebba579b6802932dde9b5f71bb9bbebd
# Parent  97d6472dd3024955a39c9d1c0bee2a702290ff92
tuned quickcheck generator for bool

diff -r 97d6472dd302 -r a6e982b1ebba src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Jul 10 07:59:23 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Fri Jul 10 07:59:25 2009 +0200
@@ -23,8 +23,8 @@
 begin
 
 definition
-  "random i = Random.range i o\<rightarrow>
-    (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
+  "random i = Random.range 2 o\<rightarrow>
+    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
 
 instance ..
 
@@ -97,7 +97,7 @@
   \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
 
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+instantiation "fun" :: ("{eq, term_of}", random) random
 begin
 
 definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where