--- 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 ("?")
--- 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"} $