--- 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))