# HG changeset patch
# User oheimb
# Date 878912698 -3600
# Node ID 71a79ac5516f3d90e15edcab0dee7a934b614910
# Parent  23a09f2fd687f414e51d0c7464922be7692d231b
added exists_Const

diff -r 23a09f2fd687 -r 71a79ac5516f 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)