--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 12:09:29 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 15:07:10 2011 +0100
@@ -537,7 +537,9 @@
code_const catch_match'
(Quickcheck "(_) handle Match => _")
-consts unknown :: "'a" ("?")
+axiomatization unknown :: 'a
+
+notation (output) unknown ("?")
use "Tools/Quickcheck/exhaustive_generators.ML"
@@ -547,7 +549,7 @@
hide_fact orelse_def catch_match_def
no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse catch_match mk_map_term check_all_n_lists
+hide_const (open) orelse catch_match catch_match' 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