# HG changeset patch
# User wenzelm
# Date 1122916837 -7200
# Node ID c895701d55eaf486a5a91ada52407020348bcfd3
# Parent  4600e74aeb0d43cff79826ed9f58df5417ea7dab
replaced atless by term_ord;

diff -r 4600e74aeb0d -r c895701d55ea src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Aug 01 19:20:36 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Aug 01 19:20:37 2005 +0200
@@ -129,7 +129,7 @@
 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 (make_ord atless) (term_frees t);
+fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
 
 fun forall_intr (t, prop) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
diff -r 4600e74aeb0d -r c895701d55ea src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Aug 01 19:20:36 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 01 19:20:37 2005 +0200
@@ -31,14 +31,14 @@
   in all T $ Abs (a, T, abstract_over (t, prop)) end;
 
 fun forall_intr_vfs prop = foldr forall_intr prop
-  (vars_of prop @ sort (make_ord atless) (term_frees prop));
+  (vars_of prop @ sort Term.term_ord (term_frees prop));
 
 fun forall_intr_prf (t, prf) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   in Abst (a, SOME T, prf_abstract_over t prf) end;
 
 fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
-  (vars_of prop @ sort (make_ord atless) (term_frees prop));
+  (vars_of prop @ sort Term.term_ord (term_frees prop));
 
 fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
   (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
diff -r 4600e74aeb0d -r c895701d55ea src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Aug 01 19:20:36 2005 +0200
+++ b/src/Pure/drule.ML	Mon Aug 01 19:20:37 2005 +0200
@@ -379,7 +379,7 @@
 fun forall_intr_frees th =
     let val {prop,thy,...} = rep_thm th
     in  forall_intr_list
-         (map (cterm_of thy) (sort (make_ord atless) (term_frees prop)))
+         (map (cterm_of thy) (sort Term.term_ord (term_frees prop)))
          th
     end;
 
diff -r 4600e74aeb0d -r c895701d55ea src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Aug 01 19:20:36 2005 +0200
+++ b/src/Pure/proofterm.ML	Mon Aug 01 19:20:37 2005 +0200
@@ -824,7 +824,7 @@
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if ixn mem nvs then SOME v else NONE) (vars_of prop) @
-      map SOME (sort (make_ord atless) (term_frees prop));
+      map SOME (sort Term.term_ord (term_frees prop));
   in
     proof_combt' (c (name, prop, NONE), args)
   end;
@@ -1123,7 +1123,7 @@
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if ixn mem nvs then SOME v else NONE) (vars_of prop) @
-      map SOME (sort (make_ord atless) (term_frees prop));
+      map SOME (sort Term.term_ord (term_frees prop));
     val opt_prf = if ! proofs = 2 then
         #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
           (foldr (uncurry implies_intr_proof) prf hyps)))