more direct loose_bvar1;
tuned;
slight re-unification of clone (cf. 47f8bfe0f597);

--- a/src/FOLP/hypsubst.ML	Sat Mar 26 16:21:41 2011 +0100
+++ b/src/FOLP/hypsubst.ML	Sat Mar 26 19:16:20 2011 +0100
@@ -33,24 +33,26 @@
 
 exception EQ_VAR;
 
-fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0;
-
 (*It's not safe to substitute for a constant; consider 0=1.
   It's not safe to substitute for x=t[x] since x is not eliminated.
   It's not safe to substitute for a Var; what if it appears in other goals?
   It's not safe to substitute for a variable free in the premises,
     but how could we check for this?*)
-fun inspect_pair bnd (t,u) =
-  case (Envir.eta_contract t, Envir.eta_contract u) of
-       (Bound i, _) => if loose(i,u) then raise Match
-                       else sym         (*eliminates t*)
-     | (_, Bound i) => if loose(i,t) then raise Match
-                       else asm_rl      (*eliminates u*)
-     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
-                      else sym          (*eliminates t*)
-     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
-                      else asm_rl       (*eliminates u*)
-     | _ => raise Match;
+fun inspect_pair bnd (t, u) =
+  (case (Envir.eta_contract t, Envir.eta_contract u) of
+    (Bound i, _) =>
+      if loose_bvar1 (u, i) then raise Match
+      else sym         (*eliminates t*)
+   | (_, Bound i) =>
+      if loose_bvar (t, i) then raise Match
+      else asm_rl      (*eliminates u*)
+   | (Free _, _) =>
+      if bnd orelse Logic.occs (t, u) then raise Match
+      else sym          (*eliminates t*)
+   | (_, Free _) =>
+      if bnd orelse Logic.occs(u,t) then raise Match
+      else asm_rl       (*eliminates u*)
+   | _ => raise Match);
 
 (*Locates a substitutable variable on the left (resp. right) of an equality
    assumption.  Returns the number of intervening assumptions, paried with