src/HOL/Lazy_Sequence.thy

--- a/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
@@ -208,7 +208,7 @@
 subsection {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
-types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
+type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
 
 definition hit_bound :: "'a hit_bound_lazy_sequence"
 where