# HG changeset patch
# User bulwahn
# Date 1322662030 -3600
# Node ID 3b7c35a08723890b7c5ceff46f6ed5ac66388bac
# Parent  d1e716cc3b8462c19c85251550db4192efcce3b0
more stable introduction of the internally used unknown term

diff -r d1e716cc3b84 -r 3b7c35a08723 src/HOL/Quickcheck_Exhaustive.thy
--- 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