src/HOL/Quickcheck.thy

 header {* A simple counterexample generator performing random testing *}
 
 theory Quickcheck
 imports Random Code_Evaluation Enum
 uses
-  "Tools/Quickcheck/quickcheck_common.ML"
+  ("Tools/Quickcheck/quickcheck_common.ML")
   ("Tools/Quickcheck/random_generators.ML")
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
+setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
+
+subsection {* Catching Match exceptions *}
+
+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 => _")
 
 subsection {* The @{text random} class *}
 
 class random = typerep +
   fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"

   assumes "random_aux 0 = rhs 0"
     and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
+subsection {* Deriving random generators for datatypes *}
+
+use "Tools/Quickcheck/quickcheck_common.ML" 
 use "Tools/Quickcheck/random_generators.ML"
 setup Random_Generators.setup
 
 
 subsection {* Code setup *}