# HG changeset patch # User berghofe # Date 1120220401 -7200 # Node ID 40b96a501773393ec686ddd1cbbbca48ee86ab78 # Parent bd4f7149ba1e01992a51eecba676e20ef85c6c7a Changed interface of Envir.lookup' diff -r bd4f7149ba1e -r 40b96a501773 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Fri Jul 01 14:19:36 2005 +0200 +++ b/src/Pure/pattern.ML Fri Jul 01 14:20:01 2005 +0200 @@ -358,7 +358,7 @@ fun mtch (instsp as (tyinsts,insts)) = fn (Var(ixn,T), t) => if loose_bvar(t,0) then raise MATCH - else (case Envir.lookup' (instsp, (ixn, T)) of + else (case Envir.lookup' (insts, (ixn, T)) of NONE => (typ_match tsig (tyinsts, (T, fastype_of t)), Vartab.update_new ((ixn, (T, t)), insts)) | SOME u => if t aeconv u then instsp else raise MATCH) @@ -414,7 +414,7 @@ in case ph of Var(ixn,T) => let val is = ints_of pargs - in case Envir.lookup' (env, (ixn, T)) of + in case Envir.lookup' (itms, (ixn, T)) of NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj)) | SOME u => if obj aeconv (red u is []) then env else raise MATCH