# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1530707187 -7200
# Node ID 1df516bffaa30094b51b1a2cc5bb8b74e1b1a8e9
# Parent  1148f63304f41fabf8bb579f794669fb7648f7b5# Parent  006da53a8ac1178763975b269c52c5ca38ca6334
merged

diff -r 006da53a8ac1 -r 1df516bffaa3 src/HOL/Quickcheck_Random.thy
--- 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