# 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