--- a/src/Pure/Proof/extraction.ML Sat Nov 15 21:31:37 2008 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Nov 16 18:18:45 2008 +0100
@@ -125,8 +125,9 @@
fun msg d s = priority (Symbol.spaces d ^ s);
-fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
-fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
+fun vars_of t = map Var (rev (Term.add_vars t []));
+fun frees_of t = map Free (rev (Term.add_frees t []));
+fun vfs_of t = vars_of t @ frees_of t;
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)