src/Pure/term.ML

   val term_tvars: term -> (indexname * sort) list
   val add_term_tycons: term * string list -> string list
   val add_term_vars: term * term list -> term list
   val term_vars: term -> term list
   val exists_Const: (string * typ -> bool) -> term -> bool
+  val exists_subterm: (term -> bool) -> term -> bool
   val compress_type: typ -> typ
   val compress_term: term -> term
 end;
 
 signature TERM =

 	|   ex (t $ u        ) = ex t orelse ex u
 	|   ex (Abs (_, _, t)) = ex t
 	|   ex _               = false
     in ex t end;
 
+fun exists_subterm P =
+  let fun ex t = P t orelse
+                 (case t of
+                    u $ v        => ex u orelse ex v
+                  | Abs(_, _, u) => ex u
+                  | _            => false)
+  in ex end;
+
 (*map classes, tycons*)
 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);