src/Pure/unify.ML

--- a/src/Pure/unify.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/unify.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -588,8 +588,8 @@
      val dps = map (fn(t,u)=> ([],t,u)) tus
   in add_unify 1 ((env, dps), Seq.empty) end;
 
-fun unifiers params =
-  Seq.cons ((Pattern.unify params, []), Seq.empty)
+fun unifiers (params as (thy, env, tus)) =
+  Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
     handle Pattern.Unif => Seq.empty
          | Pattern.Pattern => hounifiers params;