diff --git a/src/ast.rs b/src/ast.rs
index 6a68381..e1e69e5 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -11,8 +11,6 @@ impl FunctionDeclaration
 {
 	pub fn is_built_in(&self) -> bool
 	{
-		use foliage::flavor::FunctionDeclaration;
-
 		self.declaration.name.starts_with("f__") && self.declaration.name.ends_with("__")
 	}
 }
diff --git a/src/error.rs b/src/error.rs
index a0250ac..738ed3e 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -27,7 +27,6 @@ pub enum Kind
 	NoCompletedDefinitionFound(std::rc::Rc<crate::PredicateDeclaration>),
 	CannotHidePredicate(std::rc::Rc<crate::PredicateDeclaration>),
 	PredicateShouldNotOccurInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
-	WriteTPTPProgram,
 	RunVampire,
 	// TODO: rename to something Vampire-specific
 	ProveProgram(Option<i32>, String, String),
@@ -175,11 +174,6 @@ impl Error
 		Self::new(Kind::PredicateShouldNotOccurInSpecification(predicate_declaration))
 	}
 
-	pub(crate) fn new_write_tptp_program<S: Into<Source>>(source: S) -> Self
-	{
-		Self::new(Kind::WriteTPTPProgram).with(source)
-	}
-
 	pub(crate) fn new_run_vampire<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::RunVampire).with(source)
@@ -239,7 +233,6 @@ impl std::fmt::Debug for Error
 			Kind::VariableNameNotAllowed(ref variable_name) => write!(formatter,
 				"variable name “{}” not allowed (program variables must start with X, Y, or Z and integer variables with I, J, K, L, M, or N)",
 				variable_name),
-			Kind::WriteTPTPProgram => write!(formatter, "error writing TPTP program"),
 			Kind::FormulaNotClosed(free_variable_declarations) =>
 			{
 				write!(formatter, "formula may not contain free variables (free variables in this formula: ")?;
diff --git a/src/problem.rs b/src/problem.rs
index c49572a..310a15c 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -16,9 +16,6 @@ pub enum ProofResult
 	Disproven,
 }
 
-type VariableDeclarationIDs
-	= std::collections::BTreeMap::<std::rc::Rc<crate::VariableDeclaration>, usize>;
-
 pub struct Problem
 {
 	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,