src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40049 75d9f57123d6
parent 40048 f3a46d524101
child 40051 b6acda4d1c29
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:07 2010 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4      | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     1.5    val negative_compilation_of : compilation -> compilation
     1.6    val compilation_for_polarity : bool -> compilation -> compilation
     1.7 +  val is_depth_limited_compilation : compilation -> bool 
     1.8    val string_of_compilation : compilation -> string
     1.9    val compilation_names : (string * compilation) list
    1.10    val non_random_compilations : compilation list
    1.11 @@ -646,6 +647,9 @@
    1.12    | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
    1.13    | compilation_for_polarity _ c = c
    1.14  
    1.15 +fun is_depth_limited_compilation c =
    1.16 +  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq)
    1.17 +
    1.18  fun string_of_compilation c =
    1.19    case c of
    1.20      Pred => ""