--- a/src/HOL/Enum.thy Wed Dec 08 16:47:57 2010 +0100
+++ b/src/HOL/Enum.thy Wed Dec 08 18:07:03 2010 +0100
@@ -545,7 +545,7 @@
end
-hide_const a\<^isub>1
+hide_const (open) a\<^isub>1
datatype finite_2 = a\<^isub>1 | a\<^isub>2
@@ -598,7 +598,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2
+hide_const (open) a\<^isub>1 a\<^isub>2
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
@@ -651,7 +651,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
@@ -687,7 +687,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
@@ -724,10 +724,10 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
-hide_type finite_1 finite_2 finite_3 finite_4 finite_5
+hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
end