removing catch_match' now that catch_match is polymorphic
authorbulwahn
Thu Dec 01 22:16:23 2011 +0100 (2011-12-01)
changeset 45732ac5775bbc748
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
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:23 2011 +0100
     1.3 @@ -523,13 +523,6 @@
     1.4  
     1.5  subsection {* Defining combinators for any first-order data type *}
     1.6  
     1.7 -definition catch_match' :: "term => term => term"
     1.8 -where
     1.9 -  [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.10 -
    1.11 -code_const catch_match'
    1.12 -  (Quickcheck "(_) handle Match => _")
    1.13 -
    1.14  axiomatization unknown :: 'a
    1.15  
    1.16  notation (output) unknown  ("?")
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:16:23 2011 +0100
     2.3 @@ -329,7 +329,7 @@
     2.4  
     2.5  fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
     2.6  
     2.7 -fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
     2.8 +fun mk_safe_term t = @{term "Quickcheck.catch_match :: term => term => term"}
     2.9        $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
    2.10  
    2.11  fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $