--- a/src/HOL/Enum.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Enum.thy Sun Sep 14 22:59:30 2014 +0200
@@ -491,9 +491,9 @@
subsection {* Small finite types *}
-text {* We define small finite types for the use in Quickcheck *}
+text {* We define small finite types for use in Quickcheck *}
-datatype finite_1 = a\<^sub>1
+datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +595,7 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype finite_2 = a\<^sub>1 | a\<^sub>2
+datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -701,7 +701,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -825,7 +825,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -926,8 +926,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-
-datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")