# HG changeset patch
# User bulwahn
# Date 1322774186 -3600
# Node ID 6bb30ae1abfeee0c83a62eaaf9d6fa351f7ea1be
# Parent  ac5775bbc748a5f5b73d43276feee8ed019b5480
hiding internal constants and facts more properly

diff -r ac5775bbc748 -r 6bb30ae1abfe src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Dec 01 22:16:23 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Thu Dec 01 22:16:26 2011 +0100
@@ -157,6 +157,9 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
+hide_fact catch_match_def
+hide_const (open) catch_match
+
 subsection {* The Random-Predicate Monad *} 
 
 fun iter' ::
diff -r ac5775bbc748 -r 6bb30ae1abfe src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:23 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:26 2011 +0100
@@ -533,9 +533,9 @@
 
 declare [[quickcheck_batch_tester = exhaustive]]
 
-hide_fact orelse_def catch_match_def
+hide_fact orelse_def
 no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists 
+hide_const (open) orelse unknown mk_map_term check_all_n_lists 
 
 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not