# HG changeset patch
# User huffman
# Date 1318943946 -7200
# Node ID 5e4a1270c000343bf676dd5f2d9a48171fc9c679
# Parent  699848baf70b2346bdcf47bb46dbe7d4affdef06
hide typedef-generated constants Product_Type.prod and Sum_Type.sum

diff -r 699848baf70b -r 5e4a1270c000 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Product_Type.thy	Tue Oct 18 15:19:06 2011 +0200
@@ -1228,4 +1228,6 @@
 
 lemmas Pair_fst_snd_eq = prod_eq_iff
 
+hide_const (open) prod
+
 end
diff -r 699848baf70b -r 5e4a1270c000 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Sum_Type.thy	Tue Oct 18 15:19:06 2011 +0200
@@ -209,4 +209,6 @@
 
 hide_const (open) Suml Sumr Projl Projr
 
+hide_const (open) sum
+
 end
diff -r 699848baf70b -r 5e4a1270c000 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Tue Oct 18 15:19:06 2011 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) implies union inter subset sum quotient
+hide_const (open) implies union inter subset quotient
 
 text {*
   Test data for the MESON proof procedure