--- 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))
--- 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
--- 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])