# HG changeset patch
# User bulwahn
# Date 1290422107 -3600
# Node ID 58a6ba7ccfc597a979a5017e05c321e7d1dd36a0
# Parent  36ca3fad1f31c4a5547491e608351fffb4794ce7
hiding the constants

diff -r 36ca3fad1f31 -r 58a6ba7ccfc5 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Nov 22 11:35:06 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:35:07 2010 +0100
@@ -348,6 +348,8 @@
 
 end
 
+hide_const a\<^isub>1
+
 datatype finite_2 = a\<^isub>1 | a\<^isub>2
 
 instantiation finite_2 :: enum
@@ -381,6 +383,8 @@
 
 end
 
+hide_const a\<^isub>1 a\<^isub>2
+
 
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
@@ -413,6 +417,8 @@
 
 end
 
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
+
 
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
@@ -427,6 +433,7 @@
 
 end
 
+hide_const 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
@@ -442,6 +449,9 @@
 
 end
 
+hide_const 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_const (open) n_lists product