--- a/src/HOL/Quickcheck_Random.thy Wed Jul 04 11:00:06 2018 +0100
+++ b/src/HOL/Quickcheck_Random.thy Wed Jul 04 14:26:27 2018 +0200
@@ -20,6 +20,8 @@
code_printing
constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
+code_reserved Quickcheck Match
+
subsection \<open>The \<open>random\<close> class\<close>
class random = typerep +
@@ -63,7 +65,7 @@
instantiation String.literal :: random
begin
-definition
+definition
"random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
instance ..
@@ -207,7 +209,7 @@
subsection \<open>Deriving random generators for datatypes\<close>
-ML_file "Tools/Quickcheck/quickcheck_common.ML"
+ML_file "Tools/Quickcheck/quickcheck_common.ML"
ML_file "Tools/Quickcheck/random_generators.ML"
@@ -223,7 +225,7 @@
no_notation fcomp (infixl "\<circ>>" 60)
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
+
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
hide_fact (open) collapse_def beyond_def random_fun_lift_def