# HG changeset patch
# User wenzelm
# Date 1230678067 -3600
# Node ID 3ee4656b9e0c983dfb0ed8f8808fa18748c8fb5b
# Parent  7ee78cc8ef2c49f55e85e1cb14e3cf6418a00393
Some old-style term operations.

diff -r 7ee78cc8ef2c -r 3ee4656b9e0c src/Pure/old_term.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/old_term.ML	Wed Dec 31 00:01:07 2008 +0100
@@ -0,0 +1,36 @@
+(*  Title:      Pure/old_term.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Some old-style term operations.
+*)
+
+signature OLD_TERM =
+sig
+  val add_term_vars: term * term list -> term list
+  val term_vars: term -> term list
+  val add_term_frees: term * term list -> term list
+  val term_frees: term -> term list
+end;
+
+structure OldTerm: OLD_TERM =
+struct
+
+(*Accumulates the Vars in the term, suppressing duplicates*)
+fun add_term_vars (t, vars: term list) = case t of
+    Var   _ => OrdList.insert Term.term_ord t vars
+  | Abs (_,_,body) => add_term_vars(body,vars)
+  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
+  | _ => vars;
+
+fun term_vars t = add_term_vars(t,[]);
+
+(*Accumulates the Frees in the term, suppressing duplicates*)
+fun add_term_frees (t, frees: term list) = case t of
+    Free   _ => OrdList.insert Term.term_ord t frees
+  | Abs (_,_,body) => add_term_frees(body,frees)
+  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
+  | _ => frees;
+
+fun term_frees t = add_term_frees(t,[]);
+
+end;