# HG changeset patch
# User wenzelm
# Date 1158176491 -7200
# Node ID 7de9caf4fd78bde772829ec77f6f5f50962599d7
# Parent  448594cbd82b24ef9790608492b3c0a955cee115
added exists_type;

diff -r 448594cbd82b -r 7de9caf4fd78 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Sep 13 21:41:25 2006 +0200
+++ b/src/Pure/term.ML	Wed Sep 13 21:41:31 2006 +0200
@@ -119,6 +119,7 @@
   val add_term_consts: term * string list -> string list
   val term_consts: term -> string list
   val exists_subtype: (typ -> bool) -> typ -> bool
+  val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
   val add_term_free_names: term * string list -> string list
@@ -1007,6 +1008,16 @@
       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   in ex end;
 
+fun exists_type P =
+  let
+    fun ex (Const (_, T)) = P T
+      | ex (Free (_, T)) = P T
+      | ex (Var (_, T)) = P T
+      | ex (Bound _) = false
+      | ex (Abs (_, T, t)) = P T orelse ex t
+      | ex (t $ u) = ex t orelse ex u;
+  in ex end;
+
 fun exists_subterm P =
   let
     fun ex tm = P tm orelse