--- a/src/Pure/term.ML Sun May 29 05:23:28 2005 +0200
+++ b/src/Pure/term.ML Sun May 29 12:39:12 2005 +0200
@@ -150,6 +150,7 @@
val add_term_classes: term * class list -> class list
val add_term_consts: term * string list -> string list
val term_consts: term -> string list
+ val term_constsT: term -> (string * typ) list
val add_term_frees: term * term list -> term list
val term_frees: term -> term list
val add_term_free_names: term * string list -> string list
@@ -784,8 +785,6 @@
else a :: invent_names used b (n - 1)
end;
-
-
(** Consts etc. **)
fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
@@ -803,8 +802,15 @@
| add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
| add_term_consts (_, cs) = cs;
+fun add_term_constsT (Const c, cs) = c::cs
+ | add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs))
+ | add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs)
+ | add_term_constsT (_, cs) = cs;
+
fun term_consts t = add_term_consts(t,[]);
+fun term_constsT t = add_term_constsT(t,[]);
+
fun exists_Const P t = let
fun ex (Const c ) = P c
| ex (t $ u ) = ex t orelse ex u