src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

   val mk_not : compilation_funs -> term -> term
   val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
   val funT_of : compilation_funs -> mode -> typ -> typ
   (* Different compilations *)
   datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
-    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
-    | Pos_Generator_DSeq | Neg_Generator_DSeq
+    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq 
+    | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
   val is_depth_limited_compilation : compilation -> bool 
   val string_of_compilation : compilation -> string
   val compilation_names : (string * compilation) list

 
 (* Different compilations *)
 
 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
   | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
-    Pos_Generator_DSeq | Neg_Generator_DSeq
+    Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
 
 fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
   | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
   | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
   | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
-  | negative_compilation_of Pos_Generator_DSeq = Pos_Generator_DSeq
+  | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
+  | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
+  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS  
   | negative_compilation_of c = c
   
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
   | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | compilation_for_polarity _ c = c

   | Neg_Random_DSeq => "neg_random_dseq"
   | New_Pos_Random_DSeq => "new_pos_random dseq"
   | New_Neg_Random_DSeq => "new_neg_random_dseq"
   | Pos_Generator_DSeq => "pos_generator_dseq"
   | Neg_Generator_DSeq => "neg_generator_dseq"
-
+  | Pos_Generator_CPS => "pos_generator_cps"
+  | Neg_Generator_CPS => "neg_generator_cps"
+  
 val compilation_names = [("pred", Pred),
   ("random", Random),
   ("depth_limited", Depth_Limited),
   ("depth_limited_random", Depth_Limited_Random),
   (*("annotated", Annotated),*)
   ("dseq", DSeq),
   ("random_dseq", Pos_Random_DSeq),
   ("new_random_dseq", New_Pos_Random_DSeq),
-  ("generator_dseq", Pos_Generator_DSeq)]
+  ("generator_dseq", Pos_Generator_DSeq),
+  ("generator_cps", Pos_Generator_CPS)]
 
 val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
 
 
 val random_compilations = [Random, Depth_Limited_Random,
-  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
+  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS]
 
 (* datastructures and setup for generic compilation *)
 
 datatype compilation_funs = CompilationFuns of {
   mk_predT : typ -> typ,