--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Oct 21 19:13:11 2010 +0200
@@ -676,7 +676,8 @@
("depth_limited", Depth_Limited),
("depth_limited_random", Depth_Limited_Random),
(*("annotated", Annotated),*)
- ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
+ ("dseq", DSeq),
+ ("random_dseq", Pos_Random_DSeq),
("new_random_dseq", New_Pos_Random_DSeq),
("generator_dseq", Pos_Generator_DSeq)]