# HG changeset patch
# User bulwahn
# Date 1256630636 -3600
# Node ID d0c00b81db1da8e8d0cda0be1fffea7d87c1f861
# Parent  d9ca0c3bf680e914c826ef4c2f10dcd70860fffb
hiding randompred definitions

diff -r d9ca0c3bf680 -r d0c00b81db1d src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Tue Oct 27 09:03:56 2009 +0100
@@ -177,7 +177,7 @@
 
 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