src/HOL/Tools/TFL/usyntax.ML

 (*  Title:      HOL/Tools/TFL/usyntax.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
 Emulation of HOL's abstract syntax functions.
 *)
 
 signature USYNTAX =

 fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
 val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
 
 
 (* Need to reverse? *)
-fun gen_all tm = list_mk_forall(term_frees tm, tm);
+fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
 
 (* Destructing a cterm to a list of Terms *)
 fun strip_comb tm =
    let fun dest(M$N, A) = dest(M, N::A)
          | dest x = x