src/Pure/unify.ML
changeset 4438 ecfeff48bf0c
parent 4314 a6eb21e10090
child 8406 a217b0cd304d
     1.1 --- a/src/Pure/unify.ML	Fri Dec 19 09:57:24 1997 +0100
     1.2 +++ b/src/Pure/unify.ML	Fri Dec 19 09:58:03 1997 +0100
     1.3 @@ -540,7 +540,7 @@
     1.4      let val (Var(v,T), ts) = strip_comb t
     1.5  	val (Ts,U) = strip_type env T
     1.6  	and js = length ts - 1  downto 0
     1.7 -	val args = sort arg_less
     1.8 +	val args = sort (make_ord arg_less)
     1.9  		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
    1.10  	val ts' = map (#t) args
    1.11      in