--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 08:30:13 2010 +0100
@@ -478,7 +478,7 @@
(* Different options for compiler *)
-datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated
+datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
| Pos_Random_DSeq | Neg_Random_DSeq
@@ -493,6 +493,7 @@
Pred => ""
| Random => "random"
| Depth_Limited => "depth limited"
+ | Depth_Limited_Random => "depth limited random"
| DSeq => "dseq"
| Annotated => "annotated"
| Pos_Random_DSeq => "pos_random dseq"
@@ -571,7 +572,9 @@
val compilation_names = [("pred", Pred),
("random", Random),
- ("depth_limited", Depth_Limited), (*("annotated", Annotated),*)
+ ("depth_limited", Depth_Limited),
+ ("depth_limited_random", Depth_Limited_Random),
+ (*("annotated", Annotated),*)
("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
fun print_step options s =