src/Pure/pattern.ML
changeset 25473 812db0f215b3
parent 23222 daca4731942f
child 26831 6c3eec8157d3
     1.1 --- a/src/Pure/pattern.ML	Tue Nov 27 15:47:40 2007 +0100
     1.2 +++ b/src/Pure/pattern.ML	Tue Nov 27 15:49:25 2007 +0100
     1.3 @@ -328,9 +328,9 @@
     1.4    Types are matched on the fly*)
     1.5  fun first_order_match thy =
     1.6    let
     1.7 -    fun mtch (instsp as (tyinsts,insts)) = fn
     1.8 +    fun mtch k (instsp as (tyinsts,insts)) = fn
     1.9          (Var(ixn,T), t)  =>
    1.10 -          if loose_bvar(t,0) then raise MATCH
    1.11 +          if k > 0 andalso loose_bvar(t,0) then raise MATCH
    1.12            else (case Envir.lookup' (insts, (ixn, T)) of
    1.13                    NONE => (typ_match thy (T, fastype_of t) tyinsts,
    1.14                             Vartab.update_new (ixn, (T, t)) insts)
    1.15 @@ -341,11 +341,11 @@
    1.16            if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
    1.17        | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
    1.18        | (Abs(_,T,t), Abs(_,U,u))  =>
    1.19 -          mtch (typ_match thy (T,U) tyinsts, insts) (t,u)
    1.20 -      | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
    1.21 -      | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
    1.22 +          mtch (k + 1) (typ_match thy (T,U) tyinsts, insts) (t,u)
    1.23 +      | (f$t, g$u) => mtch k (mtch k instsp (f,g)) (t, u)
    1.24 +      | (t, Abs(_,U,u))  =>  mtch (k + 1) instsp ((incr t)$(Bound 0), u)
    1.25        | _ => raise MATCH
    1.26 -  in fn tu => fn env => mtch env tu end;
    1.27 +  in fn tu => fn env => mtch 0 env tu end;
    1.28  
    1.29  
    1.30  (* Matching of higher-order patterns *)