src/HOL/DSequence.thy

--- a/src/HOL/DSequence.thy	Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/DSequence.thy	Wed Mar 30 11:32:52 2011 +0200
@@ -7,7 +7,7 @@
 imports Lazy_Sequence Code_Numeral
 begin
 
-types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
+type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
 
 definition empty :: "'a dseq"
 where