314 Types are matched on the fly*) |
314 Types are matched on the fly*) |
315 fun first_order_match thy = |
315 fun first_order_match thy = |
316 let |
316 let |
317 fun mtch k (instsp as (tyinsts,insts)) = fn |
317 fun mtch k (instsp as (tyinsts,insts)) = fn |
318 (Var(ixn,T), t) => |
318 (Var(ixn,T), t) => |
319 if k > 0 andalso loose_bvar(t,0) then raise MATCH |
319 if k > 0 andalso Term.is_open t then raise MATCH |
320 else (case Envir.lookup' (insts, (ixn, T)) of |
320 else (case Envir.lookup' (insts, (ixn, T)) of |
321 NONE => (typ_match thy (T, fastype_of t) tyinsts, |
321 NONE => (typ_match thy (T, fastype_of t) tyinsts, |
322 Vartab.update_new (ixn, (T, t)) insts) |
322 Vartab.update_new (ixn, (T, t)) insts) |
323 | SOME u => if t aeconv u then instsp else raise MATCH) |
323 | SOME u => if t aeconv u then instsp else raise MATCH) |
324 | (Free (a,T), Free (b,U)) => |
324 | (Free (a,T), Free (b,U)) => |