src/Pure/term.ML

--- a/src/Pure/term.ML	Fri Nov 07 08:25:02 1997 +0100
+++ b/src/Pure/term.ML	Fri Nov 07 15:24:58 1997 +0100
@@ -564,6 +564,12 @@
   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   | add_term_consts (_, cs) = cs;
 
+fun exists_Const P t = let
+	fun ex (Const c      ) = P c
+	|   ex (t $ u        ) = ex t orelse ex u
+	|   ex (Abs (_, _, t)) = ex t
+	|   ex _               = false
+    in ex t end;
 
 (*map classes, tycons*)
 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)