1.1 --- a/src/Pure/unify.ML	Tue Jul 11 18:10:47 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Jul 11 23:00:35 2006 +0200
     1.3 @@ -526,7 +526,7 @@
     1.4    if eq_ix(v,w) then     (*...occur check would falsely return true!*)
     1.5        if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
     1.6        else raise TERM ("add_ffpair: Var name confusion", [t,u])
     1.7 -  else if xless(v,w) then (*prefer to update the LARGER variable*)
     1.8 +  else if Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
     1.9         clean_ffpair thy ((rbinder, u, t), (env,tpairs))
    1.10          else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
    1.11      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])