added exists_type;
authorwenzelm
Wed Sep 13 21:41:31 2006 +0200 (2006-09-13)
changeset 205317de9caf4fd78
parent 20530 448594cbd82b
child 20532 64181717e37c
added exists_type;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Sep 13 21:41:25 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Sep 13 21:41:31 2006 +0200
     1.3 @@ -119,6 +119,7 @@
     1.4    val add_term_consts: term * string list -> string list
     1.5    val term_consts: term -> string list
     1.6    val exists_subtype: (typ -> bool) -> typ -> bool
     1.7 +  val exists_type: (typ -> bool) -> term -> bool
     1.8    val exists_subterm: (term -> bool) -> term -> bool
     1.9    val exists_Const: (string * typ -> bool) -> term -> bool
    1.10    val add_term_free_names: term * string list -> string list
    1.11 @@ -1007,6 +1008,16 @@
    1.12        (case ty of Type (_, Ts) => exists ex Ts | _ => false);
    1.13    in ex end;
    1.14  
    1.15 +fun exists_type P =
    1.16 +  let
    1.17 +    fun ex (Const (_, T)) = P T
    1.18 +      | ex (Free (_, T)) = P T
    1.19 +      | ex (Var (_, T)) = P T
    1.20 +      | ex (Bound _) = false
    1.21 +      | ex (Abs (_, T, t)) = P T orelse ex t
    1.22 +      | ex (t $ u) = ex t orelse ex u;
    1.23 +  in ex end;
    1.24 +
    1.25  fun exists_subterm P =
    1.26    let
    1.27      fun ex tm = P tm orelse