diff -r f90874d3a246 -r df86080de4cb src/HOL/Predicate_Compile.thy --- a/src/HOL/Predicate_Compile.thy Thu Feb 14 17:58:28 2013 +0100 +++ b/src/HOL/Predicate_Compile.thy Thu Feb 14 15:27:10 2013 +0100 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports New_Random_Sequence Quickcheck_Exhaustive +imports Random_Sequence Quickcheck_Exhaustive keywords "code_pred" :: thy_goal and "values" :: diag begin