term.ML: add_loose_bnos now returns a list w/o duplicates.
pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)
--- a/src/Pure/pattern.ML Tue Apr 11 12:01:11 1995 +0200
+++ b/src/Pure/pattern.ML Wed Apr 12 13:53:34 1995 +0200
@@ -250,12 +250,11 @@
handle Type.TYPE_MATCH => raise MATCH;
fun mtch (tyinsts,insts) = fn
(Var(ixn,T), t) =>
- if null (loose_bnos t)
- then case assoc(insts,ixn) of
+ if loose_bvar(t,0) then raise MATCH
+ else (case assoc(insts,ixn) of
None => (typ_match (tyinsts, (T, fastype_of t)),
(ixn,t)::insts)
- | Some u => if t aconv u then (tyinsts,insts) else raise MATCH
- else raise MATCH
+ | Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
| (Free (a,T), Free (b,U)) =>
if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
| (Const (a,T), Const (b,U)) =>
--- a/src/Pure/term.ML Tue Apr 11 12:01:11 1995 +0200
+++ b/src/Pure/term.ML Wed Apr 12 13:53:34 1995 +0200
@@ -263,7 +263,7 @@
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
(Bound 0) is loose at level 0 *)
fun add_loose_bnos (Bound i, lev, js) =
- if i<lev then js else (i-lev) :: js
+ if i<lev then js else (i-lev) ins js
| add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
| add_loose_bnos (f$t, lev, js) =
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))