diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Quickcheck_Random.thy --- a/src/HOL/Quickcheck_Random.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Quickcheck_Random.thy Thu Jan 02 08:37:55 2025 +0100 @@ -17,7 +17,8 @@ code_printing constant catch_match \ (Quickcheck) "((_) handle Match => _)" -code_reserved Quickcheck Match +code_reserved + (Quickcheck) Match subsection \The \random\ class\ @@ -271,7 +272,8 @@ for this reason we use a distinguished target \Quickcheck\ not spoiling the regular trusted code generation\ -code_reserved Quickcheck Random_Generators +code_reserved + (Quickcheck) Random_Generators hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift