src/Pure/pattern.ML

--- a/src/Pure/pattern.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/pattern.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -226,7 +226,7 @@
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
                  in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
                  end;
-  in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
+  in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   if T = U then env