# HG changeset patch
# User wenzelm
# Date 1152651635 -7200
# Node ID 19871ee094b115d6220eb3e535c5a23fc3f59828
# Parent  be2d96bbf39cdc86292c656cf28220c9d0d99ef0
removed obsolete xless;

diff -r be2d96bbf39c -r 19871ee094b1 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Tue Jul 11 18:10:47 2006 +0200
+++ b/src/Pure/envir.ML	Tue Jul 11 23:00:35 2006 +0200
@@ -112,7 +112,7 @@
 fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
       Var (nT as (name', T)) =>
         if a = name' then env     (*cycle!*)
-        else if xless(a, name')  then
+        else if Term.indexname_ord (a, name') = LESS then
            (case lookup (env, nT) of  (*if already assigned, chase*)
                 NONE => update ((nT, Var (a, T)), env)
               | SOME u => vupdate ((aU, u), env))
diff -r be2d96bbf39c -r 19871ee094b1 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Jul 11 18:10:47 2006 +0200
+++ b/src/Pure/pattern.ML	Tue Jul 11 23:00:35 2006 +0200
@@ -218,7 +218,7 @@
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
                  in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
                  end;
-  in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
+  in if Term.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
 fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
diff -r be2d96bbf39c -r 19871ee094b1 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Jul 11 18:10:47 2006 +0200
+++ b/src/Pure/unify.ML	Tue Jul 11 23:00:35 2006 +0200
@@ -526,7 +526,7 @@
   if eq_ix(v,w) then     (*...occur check would falsely return true!*)
       if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
       else raise TERM ("add_ffpair: Var name confusion", [t,u])
-  else if xless(v,w) then (*prefer to update the LARGER variable*)
+  else if Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
        clean_ffpair thy ((rbinder, u, t), (env,tpairs))
         else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])