src/Pure/pattern.ML
changeset 19300 7689f81f8996
parent 18940 d8e12bf337a3
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/pattern.ML	Tue Mar 21 12:18:06 2006 +0100
     1.2 +++ b/src/Pure/pattern.ML	Tue Mar 21 12:18:07 2006 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    then let val f = Syntax.string_of_vname F
     1.5             val xs = bnames binders is
     1.6             val u = string_of_term thy env binders t
     1.7 -           val ys = bnames binders (loose_bnos t \\ is)
     1.8 +           val ys = bnames binders (subtract (op =) is (loose_bnos t))
     1.9         in tracing("Cannot unify variable " ^ f ^
    1.10                 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
    1.11                 "\nTerm contains additional bound variable(s) " ^ ys)