diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index a6cf364cd2836e2799cb7a2e6368a65d504f0bcc..ea0c64729ffd2349a13a458191e2afbdb84fa5fc 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -65,10 +65,6 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
 					OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
 					return visitSemanticNode(pair.getArgs()[1]);
 				}
-
-				default: {
-					return DefinitionType.EXPRESSION;
-				}
 			}
 		} else if (kind == UserDefinedOpKind) {
 			return visitUserdefinedOp(opApplNode);
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 92bd5ceffbe0f056d9bc9e5f1ff9dc79d1fb0c4e..bb42ae819779d828abd145faf447bd3537d2d410 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,7 +1,6 @@
 package de.tla2b.analysis;
 
 import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
 import tla2sany.semantic.*;
 import tlc2.tool.BuiltInOPs;
 
@@ -10,7 +9,9 @@ import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
 
-public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
+import static de.tla2b.global.TranslationGlobals.NEW_NAME;
+
+public class SymbolRenamer extends BuiltInOPs {
 
 	private final static Set<String> KEYWORDS = new HashSet<>();
 
@@ -286,7 +287,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
 
 		if (BBUILTIN_OPERATOR.containsKey(newName)) {
 			// a B built-in operator is defined outside a standard module
-			if (!STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+			if (!BBuiltInOPs.isBBuiltInOp(def)) {
 				return incName(BBUILTIN_OPERATOR.get(newName));
 			}
 		}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 8edc28de13f9f86496cdc60af16780e727aedda1..010a1cab64edc212aa2d77401fc6e0b3bd7afaaa 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -89,8 +89,8 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
 				if (!bConstList.contains(con))
 					continue;
 
-				TLAType defType = (TLAType) entry.getValue().getToolObject(TYPE_ID);
-				TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
+				TLAType defType = getType(entry.getValue());
+				TLAType conType = getType(con);
 				try {
 					setType(con, defType.unify(conType));
 				} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index 3a5515c11f5e69cece4e210aeb26f41790a6197f..5be9018c34cac46f8949ecc29f5816be43871154 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -1,13 +1,12 @@
 package de.tla2b.config;
 
-import de.tla2b.global.TranslationGlobals;
 import de.tla2b.types.TLAType;
 import tla2sany.semantic.AbortException;
 import tla2sany.semantic.NumeralNode;
 import tla2sany.st.TreeNode;
 import tlc2.value.impl.Value;
 
-public class TLCValueNode extends NumeralNode implements TranslationGlobals {
+public class TLCValueNode extends NumeralNode {
 
 	private final Value value;
 	private final TLAType type;