added exists_Const
authoroheimb
Fri Nov 07 15:24:58 1997 +0100 (1997-11-07)
changeset 418571a79ac5516f
parent 4184 23a09f2fd687
child 4186 e39f28f94cf8
added exists_Const
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Nov 07 08:25:02 1997 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Nov 07 15:24:58 1997 +0100
     1.3 @@ -564,6 +564,12 @@
     1.4    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
     1.5    | add_term_consts (_, cs) = cs;
     1.6  
     1.7 +fun exists_Const P t = let
     1.8 +	fun ex (Const c      ) = P c
     1.9 +	|   ex (t $ u        ) = ex t orelse ex u
    1.10 +	|   ex (Abs (_, _, t)) = ex t
    1.11 +	|   ex _               = false
    1.12 +    in ex t end;
    1.13  
    1.14  (*map classes, tycons*)
    1.15  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)