Don't ignore arguments to hole rule

Previously, Carcara didn't parse arguments to `hole` steps, to allow
for arbitrary arguments to be passed. However, if a proof is using
sharing and a term is named in the arguments of a `hole` step, Carcara
would return an error when that name was used later, since the name was
never defined.

Now, Carcara will fully parse all arguments to `hole` steps, and the
proof producers must ensure that these arguments are valid terms.

carcara/src/parser/mod.rs

@@ -910,15 +910,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
         let args = if self.current_token == Token::Keyword("args".into()) {
             self.next_token()?;
             self.expect_token(Token::OpenParen)?;
-
-            // If the rule is `hole`, we want to allow any invalid arguments, so we read the rest of
-            // the `:args` attribute without trying to parse anything
-            if rule == "hole" {
-                self.ignore_until_close_parens()?;
-                Vec::new()
-            } else {
-                self.parse_sequence(Self::parse_term, true)?
-            }
+            self.parse_sequence(Self::parse_term, true)?
         } else {
             Vec::new()
         };