--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:54 2010 +0200
@@ -427,12 +427,11 @@
| _ => error "equals_conv"
*)
-(* Different options for compiler *)
+(* 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
-
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
@@ -455,7 +454,7 @@
| Neg_Random_DSeq => "neg_random_dseq"
| New_Pos_Random_DSeq => "new_pos_random dseq"
| New_Neg_Random_DSeq => "new_neg_random_dseq"
-
+
val compilation_names = [("pred", Pred),
("random", Random),
("depth_limited", Depth_Limited),
@@ -463,7 +462,15 @@
(*("annotated", Annotated),*)
("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
("new_random_dseq", New_Pos_Random_DSeq)]
-
+
+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]
+
+(* Different options for compiler *)
+
(*datatype compilation_options =
Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)