# HG changeset patch
# User bulwahn
# Date 1322774183 -3600
# Node ID ac5775bbc748a5f5b73d43276feee8ed019b5480
# Parent  8d8c926bcffe220a21b0aa4a2e076637a55d2772
removing catch_match' now that catch_match is polymorphic

diff -r 8d8c926bcffe -r ac5775bbc748 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:23 2011 +0100
@@ -523,13 +523,6 @@
 
 subsection {* Defining combinators for any first-order data type *}
 
-definition catch_match' :: "term => term => term"
-where
-  [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
-
-code_const catch_match'
-  (Quickcheck "(_) handle Match => _")
-
 axiomatization unknown :: 'a
 
 notation (output) unknown  ("?")
diff -r 8d8c926bcffe -r ac5775bbc748 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:16:23 2011 +0100
@@ -329,7 +329,7 @@
 
 fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
 
-fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
+fun mk_safe_term t = @{term "Quickcheck.catch_match :: term => term => term"}
       $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
 
 fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $