--- a/src/Pure/term.ML Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/term.ML Mon Oct 14 10:44:32 2002 +0200
@@ -154,6 +154,7 @@
val add_typ_varnames: typ * string list -> string list
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 add_term_frees: term * term list -> term list
val term_frees: term -> term list
val add_term_free_names: term * string list -> string list
@@ -793,6 +794,8 @@
| add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
| add_term_consts (_, cs) = cs;
+fun term_consts t = add_term_consts(t,[]);
+
fun exists_Const P t = let
fun ex (Const c ) = P c
| ex (t $ u ) = ex t orelse ex u