src/HOL/DSequence.thy

--- a/src/HOL/DSequence.thy	Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/DSequence.thy	Mon Nov 12 23:24:40 2012 +0100
@@ -4,7 +4,7 @@
 header {* Depth-Limited Sequences with failure element *}
 
 theory DSequence
-imports Lazy_Sequence Code_Numeral
+imports Lazy_Sequence
 begin
 
 type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"