diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index e067ee3a6676b1b6254c27609de4d73ee0e08499..87c49ddf3d06cf83189095146e5dce09192d741c 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -7,13 +7,12 @@ import de.tla2b.types.TLAType;
 import de.tla2bAst.BAstCreator;
 import tla2sany.semantic.*;
 import tlc2.tool.BuiltInOPs;
-import tlc2.tool.ToolGlobals;
 
 import java.util.*;
 import java.util.Map.Entry;
 import java.util.stream.Collectors;
 
-public class BOperation extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
+public class BOperation extends BuiltInOPs implements TranslationGlobals {
 	private final String name;
 	private final OpApplNode node;
 	private final List<OpApplNode> existQuans;
diff --git a/src/main/java/de/tla2b/global/OperatorTypes.java b/src/main/java/de/tla2b/global/OperatorTypes.java
index 8d8c797ac3cda1f992bab48f352e3bc8f5d6d858..2253bcbb3aea96e3226be5350a3698c56f7c1b6a 100644
--- a/src/main/java/de/tla2b/global/OperatorTypes.java
+++ b/src/main/java/de/tla2b/global/OperatorTypes.java
@@ -1,11 +1,9 @@
 package de.tla2b.global;
 
-import tlc2.tool.ToolGlobals;
-
 import java.util.HashSet;
 import java.util.Set;
 
-public class OperatorTypes implements ToolGlobals, BBuildIns {
+public class OperatorTypes implements BBuildIns {
 	private static final Set<Integer> TLA_Predicate_Operators;
 	private static final Set<Integer> BBuiltIn_Predicate_Operators;
 
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index fcbf6c33ca281a5a01f442d503a282547930f8a5..1f2beb7db80781c8920c5b0e2e37d00c8822092e 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -11,7 +11,7 @@ import tlc2.tool.ToolGlobals;
 import java.util.HashSet;
 import java.util.Set;
 
-public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
+public class BDefinitionsFinder extends AbstractASTVisitor {
 	private final Set<OpDefNode> bDefinitionsSet = new HashSet<>();
 
 	public BDefinitionsFinder(SpecAnalyser specAnalyser) {
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 4bb59e017f063afdc5967ca7a89a3c9694258d4f..162e9d538714e7c9976f61a73b8ac13b9d65b828 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -5,16 +5,15 @@ import de.tla2b.analysis.BOperation;
 import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.global.BBuildIns;
 import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
 import tla2sany.semantic.*;
 import tlc2.tool.BuiltInOPs;
-import tlc2.tool.ToolGlobals;
 import util.UniqueString;
 
 import java.util.ArrayList;
 
-public class OperationsFinder extends AbstractASTVisitor implements
-	ASTConstants, ToolGlobals, TranslationGlobals {
+import static de.tla2b.global.TranslationGlobals.SUBSTITUTE_PARAM;
+
+public class OperationsFinder extends AbstractASTVisitor {
 	private final SpecAnalyser specAnalyser;
 
 	private String currentName;