diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
index b5ea4b4d54d892c2eb5becd305b60578952e8a7f..8ad88b7bd290b382ca564ea9fa54fa5c98d06384 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
@@ -1,6 +1,9 @@
 package de.prob.eventb.disprover.core;
 
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
 import org.eventb.core.seqprover.IReasonerInput;
+import org.eventb.core.seqprover.ITranslatableReasonerInput;
 import org.eventb.core.seqprover.proofBuilder.ReplayHints;
 
 /**
@@ -11,7 +14,8 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints;
  * 
  * @author jastram
  */
-public class DisproverReasonerInput implements IReasonerInput {
+public class DisproverReasonerInput implements IReasonerInput,
+		ITranslatableReasonerInput {
 	@Override
 	public void applyHints(ReplayHints renaming) {
 		// TODO Auto-generated method stub
@@ -29,4 +33,16 @@ public class DisproverReasonerInput implements IReasonerInput {
 		return false;
 	}
 
+	@Override
+	public ITypeEnvironment getTypeEnvironment(FormulaFactory arg0) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public IReasonerInput translate(FormulaFactory arg0) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
 }
diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
index 4a7f8d2fcc8f0d61e51139220aeaf41e9a8228ed..f7802e0351a3796fe26e079c5b74d453bbbda195 100644
--- a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
+++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
@@ -3,12 +3,14 @@ package de.prob.eventb.disprover.ui;
 import java.util.Collections;
 import java.util.List;
 
+import org.eclipse.swt.graphics.Image;
 import org.eventb.core.ast.Predicate;
 import org.eventb.core.seqprover.IProofTreeNode;
 import org.eventb.core.seqprover.IReasonerInput;
 import org.eventb.core.seqprover.ITactic;
 import org.eventb.core.seqprover.tactics.BasicTactics;
 import org.eventb.ui.prover.DefaultTacticProvider;
+import org.eventb.ui.prover.IPredicateApplication;
 import org.eventb.ui.prover.ITacticApplication;
 
 import de.prob.eventb.disprover.core.Disprover;
@@ -20,22 +22,10 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
 		return false;
 	}
 
-	protected static class MyPredicateApplication implements ITacticApplication {
-
-		private final IProofTreeNode node;
-
-		public MyPredicateApplication(IProofTreeNode node) {
-			this.node = node;
-		}
-
+	protected static class MyPredicateApplication implements
+			IPredicateApplication {
 		@Override
 		public ITactic getTactic(String[] inputs, String globalInput) {
-			return getTactic(node, globalInput, inputs);
-		}
-
-		public ITactic getTactic(IProofTreeNode node, String globalInput,
-				String[] inputs) {
-
 			IReasonerInput reasonerInput = new DisproverReasonerInput();
 			return BasicTactics.reasonerTac(
 					Disprover.createDisproverReasoner(), reasonerInput);
@@ -46,6 +36,18 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
 			return "de.prob.eventb.disprover.ui.disproverTactic";
 		}
 
+		@Override
+		public Image getIcon() {
+			// TODO Auto-generated method stub
+			return null;
+		}
+
+		@Override
+		public String getTooltip() {
+			// TODO Auto-generated method stub
+			return null;
+		}
+
 	}
 
 	public DisproverTacticProvider() {
@@ -57,7 +59,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
 			IProofTreeNode node, Predicate hyp, String globalInput) {
 
 		if (node != null && node.isOpen()) {
-			ITacticApplication application = new MyPredicateApplication(node);
+			ITacticApplication application = new MyPredicateApplication();
 			return Collections.singletonList(application);
 		}
 		return Collections.<ITacticApplication> emptyList();