removing catch_match' now that catch_match is polymorphic
authorbulwahn
Thu, 01 Dec 2011 22:16:23 +0100
changeset 45732 ac5775bbc748
parent 45731 8d8c926bcffe
child 45733 6bb30ae1abfe
removing catch_match' now that catch_match is polymorphic
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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"} $