src/Pure/Proof/extraction.ML
changeset 28812 413695e07bd4
parent 28805 8136e5736808
child 28814 463c9e9111ae
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 15 21:31:37 2008 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 16 18:18:45 2008 +0100
     1.3 @@ -125,8 +125,9 @@
     1.4  
     1.5  fun msg d s = priority (Symbol.spaces d ^ s);
     1.6  
     1.7 -fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
     1.8 -fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
     1.9 +fun vars_of t = map Var (rev (Term.add_vars t []));
    1.10 +fun frees_of t = map Free (rev (Term.add_frees t []));
    1.11 +fun vfs_of t = vars_of t @ frees_of t;
    1.12  
    1.13  fun forall_intr_prf (t, prf) =
    1.14    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)