# HG changeset patch
# User bulwahn
# Date 1333088369 -7200
# Node ID ac625d8346b2e5b30d7c72c97afe3346b0d58f5e
# Parent  06e6f352df1bff3fddc90edfa1b9a88d0e674edb
hiding fact not so aggressively

diff -r 06e6f352df1b -r ac625d8346b2 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 30 00:01:30 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 30 08:19:29 2012 +0200
@@ -587,7 +587,7 @@
 
 use "Tools/Quickcheck/abstract_generators.ML"
 
-hide_fact orelse_def
+hide_fact (open) orelse_def
 no_notation orelse (infixr "orelse" 55)
 
 hide_fact