# HG changeset patch
# User bulwahn
# Date 1290422111 -3600
# Node ID b26afaa55a75e1b735b2d70b52e1b8b0c8106828
# Parent  5ccfc3ee7fe6f87d17ea04dc5052d85ef0da34ca
hiding enum

diff -r 5ccfc3ee7fe6 -r b26afaa55a75 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Nov 22 11:35:09 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:35:11 2010 +0100
@@ -453,6 +453,6 @@
 
 
 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
-hide_const (open) n_lists product
+hide_const (open) enum n_lists product
 
 end