--- a/src/HOL/Enum.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Enum.thy Tue Sep 16 19:23:37 2014 +0200
@@ -493,7 +493,8 @@
text {* We define small finite types for use in Quickcheck *}
-datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
+datatype (plugins only: code "quickcheck*" extraction) finite_1 =
+ a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +596,8 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
+datatype (plugins only: code "quickcheck*" extraction) 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 +703,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype (plugins only: code "quickcheck*" extraction) 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 +828,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype (plugins only: code "quickcheck*" extraction) 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,7 +930,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype (plugins only: code "quickcheck*" extraction) 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")