diff options
Diffstat (limited to 'proofs/signatures/sat.plf')
| -rw-r--r-- | proofs/signatures/sat.plf | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index b95caa8fd..8f40aa8bf 100644 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -19,8 +19,8 @@ ; code to check resolutions -(program append ((c1 clause) (c2 clause)) clause - (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2))))) +(program clause_append ((c1 clause) (c2 clause)) clause + (match c1 (cln c2) ((clc l c1') (clc l (clause_append c1' c2))))) ; we use marks as follows: ; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. @@ -49,7 +49,7 @@ (match m (tt (do (ifmarked4 v v (markvar4 v)) c')) (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) - ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2))) ((clr l c1) (match l ; set mark 1 to indicate we should remove v, and fail if |