author | oheimb |
Fri, 07 Nov 1997 15:24:58 +0100 | |
changeset 4185 | 71a79ac5516f |
parent 4184 | 23a09f2fd687 |
child 4186 | e39f28f94cf8 |
src/Pure/term.ML | file | annotate | diff | comparison | revisions |
--- 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)