diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
index 1c7f3f8c8ecf5220c35770faf0e2d09d5a775647..08d812015dd3d62d87e7cd89fa53b6922afec3d3 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
@@ -1,17 +1,31 @@
 package de.prob.eventb.disprover.core;
 
-import java.util.*;
+import java.util.HashSet;
+import java.util.Set;
 
 import org.eclipse.core.runtime.Status;
-import org.eventb.core.*;
+import org.eventb.core.IEventBProject;
+import org.eventb.core.IPOSequent;
 import org.eventb.core.ast.Predicate;
-import org.eventb.core.seqprover.*;
+import org.eventb.core.seqprover.IConfidence;
+import org.eventb.core.seqprover.IProofMonitor;
+import org.eventb.core.seqprover.IProofRule;
 import org.eventb.core.seqprover.IProofRule.IAntecedent;
-import org.rodinp.core.*;
+import org.eventb.core.seqprover.IProverSequent;
+import org.eventb.core.seqprover.IReasoner;
+import org.eventb.core.seqprover.IReasonerInput;
+import org.eventb.core.seqprover.IReasonerInputReader;
+import org.eventb.core.seqprover.IReasonerInputWriter;
+import org.eventb.core.seqprover.IReasonerOutput;
+import org.eventb.core.seqprover.ProverFactory;
+import org.eventb.core.seqprover.SerializeException;
+import org.rodinp.core.IRodinProject;
+import org.rodinp.core.RodinDBException;
 
 import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
 import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
-import de.prob.core.*;
+import de.prob.core.Animator;
+import de.prob.core.PrologException;
 import de.prob.eventb.disprover.core.internal.DisproverCommand;
 import de.prob.eventb.disprover.core.internal.ICounterExample;
 import de.prob.eventb.disprover.core.translation.DisproverContextCreator;
@@ -114,6 +128,7 @@ public class DisproverReasoner implements IReasoner {
 		return counterExample;
 	}
 
+	@SuppressWarnings("unused")
 	private String predicateToProlog(Predicate pred) {
 		PrologTermStringOutput pto = new PrologTermStringOutput();
 		TranslationVisitor v = new TranslationVisitor();
@@ -133,7 +148,7 @@ public class DisproverReasoner implements IReasoner {
 		Predicate goal = sequent.goal();
 
 		IAntecedent ante = ProverFactory.makeAntecedent(goal);
-		
+
 		if (counterExample == null) {
 			return ProverFactory.reasonerFailure(this, input,
 					"ProB: Error occurred.");
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
index 00a0ed486fb1d86e1da41d85e1599329de85318d..69ec7ed4a45beab25c77f2e88dc18517e79004c9 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
 import java.util.List;
 
 import org.eventb.core.ast.Expression;
-import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.Type;
 
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -28,13 +27,10 @@ public class DisproverIdentifier {
 
 	private final String name;
 	private final Type type;
-	private final FormulaFactory ff;
 	private final boolean givenSet;
 
-	public DisproverIdentifier(String name, Type type, boolean givenSet,
-			FormulaFactory ff) {
+	public DisproverIdentifier(String name, Type type, boolean givenSet) {
 		this.givenSet = givenSet;
-		this.ff = ff;
 		this.name = name;
 		this.type = type;
 	}
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
index dceaec2b769aff5c1e4da9d0bacca51d47ff313f..12d68b9627987a665522e08558d083d861c64185 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
@@ -1,12 +1,26 @@
 package de.prob.eventb.disprover.core.translation;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
 
-import org.eventb.core.ast.*;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
 import org.eventb.core.ast.ITypeEnvironment.IIterator;
+import org.eventb.core.ast.Predicate;
 import org.eventb.core.seqprover.IProverSequent;
 
-import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.node.AAxiomsContextClause;
+import de.be4.classicalb.core.parser.node.AConstantsContextClause;
+import de.be4.classicalb.core.parser.node.ADeferredSetSet;
+import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.ASetsContextClause;
+import de.be4.classicalb.core.parser.node.PContextClause;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.PSet;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.prob.eventb.disprover.core.internal.DisproverIdentifier;
 import de.prob.eventb.translator.internal.TranslationVisitor;
 
@@ -43,7 +57,7 @@ public class DisproverContextCreator {
 
 			DisproverIdentifier id = new DisproverIdentifier(
 					typeIterator.getName(), typeIterator.getType(),
-					typeIterator.isGivenSet(), ff);
+					typeIterator.isGivenSet());
 
 			// sets are added to the context, vars to the model
 			if (id.isGivenSet()) {