diff -r 54f4fbc77c6c -r ecfeff48bf0c src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Dec 19 09:57:24 1997 +0100
+++ b/src/Pure/unify.ML	Fri Dec 19 09:58:03 1997 +0100
@@ -540,7 +540,7 @@
     let val (Var(v,T), ts) = strip_comb t
 	val (Ts,U) = strip_type env T
 	and js = length ts - 1  downto 0
-	val args = sort arg_less
+	val args = sort (make_ord arg_less)
 		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
 	val ts' = map (#t) args
     in