src/HOL/Quickcheck.thy

   for this reason we use a distinguished target @{text Quickcheck}
   not spoiling the regular trusted code generation *}
 
 code_reserved Quickcheck Quickcheck_Generators
 
-
+hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
 hide (open) type randompred
 hide (open) const random collapse beyond random_fun_aux random_fun_lift
   empty single bind union if_randompred not_randompred Random map
 
 no_notation fcomp (infixl "o>" 60)