src/HOL/Predicate_Compile.thy

--- a/src/HOL/Predicate_Compile.thy	Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Predicate_Compile.thy	Mon Nov 12 23:24:40 2012 +0100
@@ -5,7 +5,7 @@
 header {* A compiler for predicates defined by introduction rules *}
 
 theory Predicate_Compile
-imports Predicate New_Random_Sequence Quickcheck_Exhaustive
+imports New_Random_Sequence Quickcheck_Exhaustive
 keywords "code_pred" :: thy_goal and "values" :: diag
 begin