src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40054 cd7b1fa20bce
parent 40052 ea46574ca815
child 40101 f7fc517e21c6
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:11 2010 +0200
     1.3 @@ -676,7 +676,8 @@
     1.4    ("depth_limited", Depth_Limited),
     1.5    ("depth_limited_random", Depth_Limited_Random),
     1.6    (*("annotated", Annotated),*)
     1.7 -  ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
     1.8 +  ("dseq", DSeq),
     1.9 +  ("random_dseq", Pos_Random_DSeq),
    1.10    ("new_random_dseq", New_Pos_Random_DSeq),
    1.11    ("generator_dseq", Pos_Generator_DSeq)]
    1.12