src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 48221 e0ed7fab0d09
parent 46662 4e258158be38
child 50056 72efd6b4038d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 09 09:28:26 2012 +1000
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 09 09:47:59 2012 +0200
     1.3 @@ -679,7 +679,8 @@
     1.4  
     1.5  
     1.6  val random_compilations = [Random, Depth_Limited_Random,
     1.7 -  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS]
     1.8 +  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq,
     1.9 +  Pos_Generator_CPS, Neg_Generator_CPS]
    1.10  
    1.11  (* datastructures and setup for generic compilation *)
    1.12