src/Pure/term.ML

 fun add_term_consts (Const (c, _), cs) = c ins cs
   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   | 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)
   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);