src/Pure/pattern.ML
changeset 20098 19871ee094b1
parent 20079 ec5c8584487c
child 20672 b96394d8c702
     1.1 --- a/src/Pure/pattern.ML	Tue Jul 11 18:10:47 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Jul 11 23:00:35 2006 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
     1.5                   in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
     1.6                   end;
     1.7 -  in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
     1.8 +  in if Term.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
     1.9  
    1.10  fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
    1.11    if T=U then env