src/Pure/term.ML
changeset 29265 5b4247055bd7
parent 29257 660234d959f7
child 29269 5c25a2012975
     1.1 --- a/src/Pure/term.ML	Wed Dec 31 00:08:11 2008 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*  Title:      Pure/term.ML
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   Cambridge University 1992
     1.7  
     1.8  Simply typed lambda-calculus: types, terms, and basic operations.
     1.9  *)
    1.10 @@ -132,10 +131,6 @@
    1.11    val typ_tvars: typ -> (indexname * sort) list
    1.12    val term_tfrees: term -> (string * sort) list
    1.13    val term_tvars: term -> (indexname * sort) list
    1.14 -  val add_term_vars: term * term list -> term list
    1.15 -  val term_vars: term -> term list
    1.16 -  val add_term_frees: term * term list -> term list
    1.17 -  val term_frees: term -> term list
    1.18    val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
    1.19    val show_question_marks: bool ref
    1.20  end;
    1.21 @@ -1150,27 +1145,6 @@
    1.22  fun term_tvars t = add_term_tvars(t,[]);
    1.23  
    1.24  
    1.25 -(** Frees and Vars **)
    1.26 -
    1.27 -(*Accumulates the Vars in the term, suppressing duplicates*)
    1.28 -fun add_term_vars (t, vars: term list) = case t of
    1.29 -    Var   _ => OrdList.insert term_ord t vars
    1.30 -  | Abs (_,_,body) => add_term_vars(body,vars)
    1.31 -  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
    1.32 -  | _ => vars;
    1.33 -
    1.34 -fun term_vars t = add_term_vars(t,[]);
    1.35 -
    1.36 -(*Accumulates the Frees in the term, suppressing duplicates*)
    1.37 -fun add_term_frees (t, frees: term list) = case t of
    1.38 -    Free   _ => OrdList.insert term_ord t frees
    1.39 -  | Abs (_,_,body) => add_term_frees(body,frees)
    1.40 -  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
    1.41 -  | _ => frees;
    1.42 -
    1.43 -fun term_frees t = add_term_frees(t,[]);
    1.44 -
    1.45 -
    1.46  (* dest abstraction *)
    1.47  
    1.48  fun dest_abs (x, T, body) =