1.1 --- a/src/Pure/Proof/extraction.ML	Mon Aug 01 19:20:36 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Aug 01 19:20:37 2005 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4  fun msg d s = priority (Symbol.spaces d ^ s);
     1.5  
     1.6  fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
     1.7 -fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
     1.8 +fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
     1.9  
    1.10  fun forall_intr (t, prop) =
    1.11    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)