# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1530694708 -7200
# Node ID 1148f63304f41fabf8bb579f794669fb7648f7b5
# Parent  1657b9a5dd5d3dd459b0aa6409ed4a4c481d8fdc
avoid clashes in quickcheck [random]

diff -r 1657b9a5dd5d -r 1148f63304f4 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Tue Jul 03 14:46:14 2018 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Wed Jul 04 10:58:28 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