moved quickcheck setup to distribution

--- a/src/HOL/Library/Type_Length.thy	Fri Oct 18 18:41:31 2019 +0000
+++ b/src/HOL/Library/Type_Length.thy	Fri Oct 18 18:41:33 2019 +0000
@@ -70,4 +70,37 @@
 instance bit1 :: (len0) len
   by standard simp
 
+instantiation Enum.finite_1 :: len
+begin
+
+definition
+  "len_of_finite_1 (x :: Enum.finite_1 itself) \<equiv> (1 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_1_def)
+
 end
+
+instantiation Enum.finite_2 :: len
+begin
+
+definition
+  "len_of_finite_2 (x :: Enum.finite_2 itself) \<equiv> (2 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_2_def)
+
+end
+
+instantiation Enum.finite_3 :: len
+begin
+
+definition
+  "len_of_finite_3 (x :: Enum.finite_3 itself) \<equiv> (4 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_3_def)
+
+end
+
+end

--- a/src/HOL/Word/Word.thy	Fri Oct 18 18:41:31 2019 +0000
+++ b/src/HOL/Word/Word.thy	Fri Oct 18 18:41:33 2019 +0000
@@ -286,6 +286,12 @@
 
 end
 
+quickcheck_generator word
+  constructors:
+    "zero_class.zero :: ('a::len) word",
+    "numeral :: num \<Rightarrow> ('a::len) word",
+    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"
+
 text \<open>Legacy theorems:\<close>
 
 lemma word_arith_wis [code]: