removed obsolete xless;
authorwenzelm
Tue Jul 11 23:00:35 2006 +0200 (2006-07-11)
changeset 2009819871ee094b1
parent 20097 be2d96bbf39c
child 20099 bc3f9cb33645
removed obsolete xless;
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/envir.ML	Tue Jul 11 18:10:47 2006 +0200
     1.2 +++ b/src/Pure/envir.ML	Tue Jul 11 23:00:35 2006 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
     1.5        Var (nT as (name', T)) =>
     1.6          if a = name' then env     (*cycle!*)
     1.7 -        else if xless(a, name')  then
     1.8 +        else if Term.indexname_ord (a, name') = LESS then
     1.9             (case lookup (env, nT) of  (*if already assigned, chase*)
    1.10                  NONE => update ((nT, Var (a, T)), env)
    1.11                | SOME u => vupdate ((aU, u), env))
     2.1 --- a/src/Pure/pattern.ML	Tue Jul 11 18:10:47 2006 +0200
     2.2 +++ b/src/Pure/pattern.ML	Tue Jul 11 23:00:35 2006 +0200
     2.3 @@ -218,7 +218,7 @@
     2.4                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
     2.5                   in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
     2.6                   end;
     2.7 -  in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
     2.8 +  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
     2.9  
    2.10  fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
    2.11    if T=U then env
     3.1 --- a/src/Pure/unify.ML	Tue Jul 11 18:10:47 2006 +0200
     3.2 +++ b/src/Pure/unify.ML	Tue Jul 11 23:00:35 2006 +0200
     3.3 @@ -526,7 +526,7 @@
     3.4    if eq_ix(v,w) then     (*...occur check would falsely return true!*)
     3.5        if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
     3.6        else raise TERM ("add_ffpair: Var name confusion", [t,u])
     3.7 -  else if xless(v,w) then (*prefer to update the LARGER variable*)
     3.8 +  else if Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
     3.9         clean_ffpair thy ((rbinder, u, t), (env,tpairs))
    3.10          else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
    3.11      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])