# HG changeset patch
# User paulson
# Date 879243157 -3600
# Node ID 9953c0995b79c818e40518e9563b6aa70b09c13c
# Parent  7f7bf0bd0f6345e1b240ff01c35ac7e124466e0c
Now applies "map negOfGoal" to lits when expanding haz rules.
Also improved comments

diff -r 7f7bf0bd0f63 -r 9953c0995b79 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Nov 10 15:25:12 1997 +0100
+++ b/src/Provers/blast.ML	Tue Nov 11 11:12:37 1997 +0100
@@ -677,7 +677,7 @@
 
 (*Does t occur in u?  For substitution.  
   Does NOT check args of Skolem terms: substitution does not affect them.
-  NOT reflexive since hyp_subst_tac fails on x=x.*)
+  REFLEXIVE because hyp_subst_tac fails on x=x.*)
 fun substOccur t = 
   let fun occEq u = (t aconv u) orelse occ u
       and occ (Var(ref None))    = false
@@ -696,6 +696,7 @@
 		(eta_contract_atom t, eta_contract_atom u)
   | dest_eq _                           = raise DEST_EQ;
 
+(*Reject the equality if u occurs in (or equals!) t*)
 fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
 
 (*IF the goal is an equality with a substitutable variable 
@@ -1005,8 +1006,14 @@
 	      fun newPrem (vars,recur,dup,lim') prem = 
 		  let val Gs' = map (fn P => (P,false)) prem
 		      and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
-                  in  (if recur then [(Gs',Hs')] else [(Gs',[]), ([],Hs')], 
-		       lits, vars, lim')
+		      and lits' = if (exists isGoal prem) 
+			          then map negOfGoal lits
+				  else lits
+                  in  (if recur (*send new haz premises to the BACK of the
+				  queue to prevent exclusion of others*)
+		       then [(Gs',Hs')] 
+		       else [(Gs',[]), ([],Hs')], 
+		       lits', vars, lim')
 		  end
 	      fun newBr x prems = map (newPrem x) prems  @  brs
 	      (*Seek a matching rule.  If unifiable then add new premises