src/Pure/pattern.ML
changeset 17221 6cd180204582
parent 17203 29b2563f5c11
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/pattern.ML	Thu Sep 01 16:19:02 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Sep 01 18:48:50 2005 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4            if loose_bvar(t,0) then raise MATCH
     1.5            else (case Envir.lookup' (insts, (ixn, T)) of
     1.6                    NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
     1.7 -                           Vartab.update_new ((ixn, (T, t)), insts))
     1.8 +                           Vartab.curried_update_new (ixn, (T, t)) insts)
     1.9                  | SOME u => if t aeconv u then instsp else raise MATCH)
    1.10        | (Free (a,T), Free (b,U)) =>
    1.11            if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
    1.12 @@ -378,11 +378,11 @@
    1.13  fun match_bind(itms,binders,ixn,T,is,t) =
    1.14    let val js = loose_bnos t
    1.15    in if null is
    1.16 -     then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
    1.17 +     then if null js then Vartab.curried_update_new (ixn, (T, t)) itms else raise MATCH
    1.18       else if js subset_int is
    1.19            then let val t' = if downto0(is,length binders - 1) then t
    1.20                              else mapbnd (idx is) t
    1.21 -               in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
    1.22 +               in Vartab.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end
    1.23            else raise MATCH
    1.24    end;
    1.25