--- a/src/Pure/pattern.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/pattern.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
(* Title: Pure/pattern.ML
- ID: $Id$
- Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
+ Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen
Unification of Higher-Order Patterns.
@@ -223,7 +222,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 Term.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) 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
fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
if T=U then env