# HG changeset patch
# User paulson
# Date 909133415 -7200
# Node ID bebd10cb7a8d10b989f6ebbe275a2981a8518541
# Parent  6efa861fb51019a0c920f9a8558b6165f60d72fa
occurs check now handles Bound variables (for soundness)

diff -r 6efa861fb510 -r bebd10cb7a8d src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Oct 23 10:38:20 1998 +0200
+++ b/src/Provers/blast.ML	Fri Oct 23 11:03:35 1998 +0200
@@ -323,20 +323,22 @@
   | _              => wkNormAux t;
 
 
-(*Does variable v occur in u?  For unification.*)
+(*Does variable v occur in u?  For unification.  
+  Dangling bound vars are also forbidden.*)
 fun varOccur v = 
-  let fun occL [] = false	(*same as (exists occ), but faster*)
-	| occL (u::us) = occ u orelse occL us
-      and occ (Var w) = 
+  let fun occL lev [] = false	(*same as (exists occ), but faster*)
+	| occL lev (u::us) = occ lev u orelse occL lev us
+      and occ lev (Var w) = 
 	      v=w orelse
               (case !w of None   => false
-	                | Some u => occ u)
-        | occ (Skolem(_,args)) = occL (map Var args)
-        | occ (TConst(_,u)) = occ u
-        | occ (Abs(_,u)) = occ u
-        | occ (f$u)      = occ u  orelse  occ f
-        | occ (_)        = false;
-  in  occ  end;
+	                | Some u => occ lev u)
+        | occ lev (Skolem(_,args)) = occL lev (map Var args)
+            (*ignore TConst, since term variables can't occur in types (?) *)
+        | occ lev (Bound i)  = lev <= i
+        | occ lev (Abs(_,u)) = occ (lev+1) u
+        | occ lev (f$u)      = occ lev u  orelse  occ lev f
+        | occ lev _          = false;
+  in  occ 0  end;
 
 exception UNIFY;