# HG changeset patch
# User wenzelm
# Date 1301163380 -3600
# Node ID a8cbb93711546f9af4d19b68968582e0287b6ab5
# Parent  7519c7c33017a8d0d30763b86beb84fba5f048e8
more direct loose_bvar1;
tuned;
slight re-unification of clone (cf. 47f8bfe0f597);

diff -r 7519c7c33017 -r a8cbb9371154 src/FOLP/hypsubst.ML
--- 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