src/HOL/Quickcheck_Random.thy

--- a/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -168,7 +168,7 @@
 instantiation set :: (random) random
 begin
 
-primrec random_aux_set
+fun random_aux_set
 where
   "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
 | "random_aux_set (Code_Numeral.Suc i) j =