src/Pure/pattern.ML
changeset 16651 40b96a501773
parent 15797 a63605582573
child 16668 fdb4992cf1d2
     1.1 --- a/src/Pure/pattern.ML	Fri Jul 01 14:19:36 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri Jul 01 14:20:01 2005 +0200
     1.3 @@ -358,7 +358,7 @@
     1.4      fun mtch (instsp as (tyinsts,insts)) = fn
     1.5          (Var(ixn,T), t)  =>
     1.6            if loose_bvar(t,0) then raise MATCH
     1.7 -          else (case Envir.lookup' (instsp, (ixn, T)) of
     1.8 +          else (case Envir.lookup' (insts, (ixn, T)) of
     1.9                    NONE => (typ_match tsig (tyinsts, (T, fastype_of t)),
    1.10                             Vartab.update_new ((ixn, (T, t)), insts))
    1.11                  | SOME u => if t aeconv u then instsp else raise MATCH)
    1.12 @@ -414,7 +414,7 @@
    1.13      in case ph of
    1.14           Var(ixn,T) =>
    1.15             let val is = ints_of pargs
    1.16 -           in case Envir.lookup' (env, (ixn, T)) of
    1.17 +           in case Envir.lookup' (itms, (ixn, T)) of
    1.18                  NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
    1.19                | SOME u => if obj aeconv (red u is []) then env
    1.20                            else raise MATCH