# HG changeset patch
# User bulwahn
# Date 1264156948 -3600
# Node ID 3b1957113753dfe3a6cec48e3ae9ae578454df5f
# Parent  fac9d03117252f50f24ae2cbc9c62bbe76b85270
correctly hiding facts of Lazy_Sequence

diff -r fac9d0311725 -r 3b1957113753 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Thu Jan 21 14:13:21 2010 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Fri Jan 22 11:42:28 2010 +0100
@@ -153,6 +153,6 @@
 
 hide (open) type lazy_sequence
 hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
-hide (open) fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
+hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
 
 end