adding a missing entry to predicate compiler's setup
authorbulwahn
Mon Jul 09 09:47:59 2012 +0200 (2012-07-09)
changeset 48221e0ed7fab0d09
parent 48211 12bbb9d4b6ed
child 48222 fcca68383808
adding a missing entry to predicate compiler's setup
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     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