src/HOL/Enum.thy
changeset 41085 a549ff1d4070
parent 41078 051251fde456
child 41115 2c362ff5daf4
--- 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