src/Pure/pattern.ML

--- a/src/Pure/pattern.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/pattern.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -316,7 +316,7 @@
   let
     fun mtch k (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
-          if k > 0 andalso loose_bvar(t,0) then raise MATCH
+          if k > 0 andalso Term.is_open t then raise MATCH
           else (case Envir.lookup' (insts, (ixn, T)) of
                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
                            Vartab.update_new (ixn, (T, t)) insts)