src/Pure/unify.ML
changeset 20098 19871ee094b1
parent 20083 717b1eb434f1
child 20548 8ef25fe585a8
--- 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])