--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 22:14:35 2011 +0100
@@ -523,13 +523,6 @@
subsection {* Defining combinators for any first-order data type *}
-definition catch_match :: "term list option => term list option => term list option"
-where
- [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
-
-code_const catch_match
- (Quickcheck "(_) handle Match => _")
-
definition catch_match' :: "term => term => term"
where
[code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"