changeset 4438 | ecfeff48bf0c |
parent 4314 | a6eb21e10090 |
child 8406 | a217b0cd304d |
--- 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