diff -r 6da283e4497b -r 94041d602ecb src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Mon Nov 12 18:42:49 2012 +0100 +++ b/src/HOL/Lazy_Sequence.thy Mon Nov 12 23:24:40 2012 +0100 @@ -4,7 +4,7 @@ header {* Lazy sequences *} theory Lazy_Sequence -imports List Code_Numeral +imports Predicate begin datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"