src/HOL/Random_Sequence.thy

--- a/src/HOL/Random_Sequence.thy	Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Random_Sequence.thy	Mon Nov 12 23:24:40 2012 +0100
@@ -2,7 +2,7 @@
 (* Author: Lukas Bulwahn, TU Muenchen *)
 
 theory Random_Sequence
-imports Quickcheck DSequence
+imports Quickcheck
 begin
 
 type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"