# HG changeset patch
# User nipkow
# Date 797687614 -7200
# Node ID 27808dabf4af62f1774116e6a78d0038d6ab732d
# Parent  88c8df00905bb37b0b1790a8cfd46d4c0d56157e
term.ML: add_loose_bnos now returns a list w/o duplicates.
pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)

diff -r 88c8df00905b -r 27808dabf4af src/Pure/pattern.ML
--- 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))  =>
diff -r 88c8df00905b -r 27808dabf4af src/Pure/term.ML
--- 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))