--- a/src/HOL/Library/Polynomial.thy Tue Dec 20 17:40:17 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy Tue Dec 20 17:40:18 2011 +0100
@@ -1503,6 +1503,8 @@
code_datatype "0::'a::zero poly" pCons
+quickcheck_generator poly constructors: "0::'a::zero poly", pCons
+
declare pCons_0_0 [code_post]
instantiation poly :: ("{zero, equal}") equal
--- a/src/HOL/Library/RBT.thy Tue Dec 20 17:40:17 2011 +0100
+++ b/src/HOL/Library/RBT.thy Tue Dec 20 17:40:18 2011 +0100
@@ -169,5 +169,8 @@
"distinct (keys t)"
by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
+subsection {* Quickcheck generators *}
+
+quickcheck_generator rbt constructors: empty, insert
end