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