src/Pure/unify.ML
changeset 18184 43c4589a9a78
parent 17344 8b2f56aff711
child 18945 0b15863018a8
     1.1 --- a/src/Pure/unify.ML	Wed Nov 16 17:45:29 2005 +0100
     1.2 +++ b/src/Pure/unify.ML	Wed Nov 16 17:45:30 2005 +0100
     1.3 @@ -588,8 +588,8 @@
     1.4       val dps = map (fn(t,u)=> ([],t,u)) tus
     1.5    in add_unify 1 ((env, dps), Seq.empty) end;
     1.6  
     1.7 -fun unifiers params =
     1.8 -  Seq.cons ((Pattern.unify params, []), Seq.empty)
     1.9 +fun unifiers (params as (thy, env, tus)) =
    1.10 +  Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
    1.11      handle Pattern.Unif => Seq.empty
    1.12           | Pattern.Pattern => hounifiers params;
    1.13