diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index fa875b8965f64d8246b6e8493498f1306cfd4017..e067ee3a6676b1b6254c27609de4d73ee0e08499 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -23,7 +23,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants, ToolGlobals,
 	private final List<OpDeclNode> unchangedVariablesList;
 	private final List<ExprOrOpArgNode> guards;
 	private final List<ExprOrOpArgNode> beforeAfterPredicates;
-	private final LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
+	private final Map<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
 	private List<OpDeclNode> anyVariables;
 	private final SpecAnalyser specAnalyser;
 
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 75ab20d472cefd96e6e9cffd60540e68c9e82f49..5c992316bf0fcaa32e4e5982767ef56c7f8d07d3 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -21,7 +21,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 	private OpDefNode spec;
 	private OpDefNode init;
 	private OpDefNode next;
-	private ArrayList<OpDefNode> invariants = new ArrayList<>();
+	private List<OpDefNode> invariants = new ArrayList<>();
 
 	private OpDefNode expressionOpdefNode;
 	private final Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>();
@@ -29,12 +29,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 	private final ModuleNode moduleNode;
 	private ExprNode nextExpr;
 
-	private ArrayList<OpDeclNode> bConstants;
+	private List<OpDeclNode> bConstants;
 	// used to check if a b constant has arguments and is not overridden in the
 	// configfile
 
-	private ArrayList<BOperation> bOperations = new ArrayList<>();
-	private final ArrayList<ExprNode> inits = new ArrayList<>();
+	private List<BOperation> bOperations = new ArrayList<>();
+	private final List<ExprNode> inits = new ArrayList<>();
 
 	private Set<OpDefNode> bDefinitionsSet = new HashSet<>();
 	// set of OpDefNodes which will appear in the resulting B Machine
@@ -43,11 +43,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 	private final Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
 	// additional parameters of a let Operator, these parameters are from the
 	// surrounding operator
-	private final ArrayList<String> definitionMacros = new ArrayList<>();
+	private final List<String> definitionMacros = new ArrayList<>();
 
-	private final ArrayList<OpDefNode> recursiveFunctions = new ArrayList<>();
+	private final List<OpDefNode> recursiveFunctions = new ArrayList<>();
 
-	private final ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
+	private final List<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
 
 	private ConfigfileEvaluator configFileEvaluator;
 
@@ -313,11 +313,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		}
 	}
 
-	public ArrayList<BOperation> getBOperations() {
+	public List<BOperation> getBOperations() {
 		return this.bOperations;
 	}
 
-	public ArrayList<ExprNode> getInits() {
+	public List<ExprNode> getInits() {
 		return this.inits;
 	}
 
@@ -333,7 +333,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		return new Hashtable<>(letParams);
 	}
 
-	public ArrayList<String> getDefinitionMacros() {
+	public List<String> getDefinitionMacros() {
 		return definitionMacros;
 	}
 
@@ -341,11 +341,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		return usedDefinitions;
 	}
 
-	public ArrayList<OpDefNode> getRecursiveFunctions() {
+	public List<OpDefNode> getRecursiveFunctions() {
 		return recursiveFunctions;
 	}
 
-	public ArrayList<RecursiveDefinition> getRecursiveDefinitions() {
+	public List<RecursiveDefinition> getRecursiveDefinitions() {
 		return recursiveDefinitions;
 	}
 
@@ -357,7 +357,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		return configFileEvaluator;
 	}
 
-	public ArrayList<OpDefNode> getInvariants() {
+	public List<OpDefNode> getInvariants() {
 		return invariants;
 	}
 
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 4f6d48b80f0579bc7ea3153ea89c7abdbb4e4a56..60404782f67d38a7ab2ae3e0281e5a57f7f11435 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -19,19 +19,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 	private static final int TEMP_TYPE_ID = 6;
 	private int paramId;
 
-	private ArrayList<ExprNode> inits;
+	private List<ExprNode> inits;
 	private ExprNode nextExpr;
 	private final Set<OpDefNode> usedDefinitions;
 	private final Set<OpDefNode> bDefinitions;
 
-	private final ArrayList<SymbolNode> symbolNodeList = new ArrayList<>();
-	private final ArrayList<SemanticNode> tupleNodeList = new ArrayList<>();
+	private final List<SymbolNode> symbolNodeList = new ArrayList<>();
+	private final List<SemanticNode> tupleNodeList = new ArrayList<>();
 
 	private final ModuleNode moduleNode;
-	private ArrayList<OpDeclNode> bConstList;
+	private List<OpDeclNode> bConstList;
 	private final SpecAnalyser specAnalyser;
 
-	private Hashtable<OpDeclNode, ValueObj> constantAssignments;
+	private Map<OpDeclNode, ValueObj> constantAssignments;
 
 	private ConfigfileEvaluator conEval;
 
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index c9e3b57e3943e8b2f489743b531f0a734043e56a..847533e1ec694053ab8e34f74ff29d50f53e2868 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -22,36 +22,35 @@ public class ConfigfileEvaluator {
 
 	private ModelConfig configAst;
 	private ModuleNode moduleNode;
-	private Hashtable<String, OpDefNode> definitions;
-	// Hashtable of all definitions in module
-	private Hashtable<String, OpDeclNode> constants;
-	// Hashtable of all constants in the module
+	private Map<String, OpDefNode> definitions;
+	// map of all definitions in module
+	private Map<String, OpDeclNode> constants;
+	// map of all constants in the module
 
 	private OpDefNode specNode; // SPECIFICATION node, may be null
 	private OpDefNode nextNode; // NEXT node, may be null
 	private OpDefNode initNode; // INIT node, may be null
-	private final ArrayList<OpDefNode> invariantNodeList = new ArrayList<>();
-	private ArrayList<String> enumeratedSet;
-	private LinkedHashMap<String, EnumType> enumeratedTypes;
-	public Hashtable<OpDeclNode, ValueObj> constantAssignments;
+	private final List<OpDefNode> invariantNodeList = new ArrayList<>();
+	private List<String> enumeratedSet;
+	private Map<String, EnumType> enumeratedTypes;
+	public Map<OpDeclNode, ValueObj> constantAssignments;
 	// k = 1, the ValueObj describes the right side of the assignment and
 	// contains it type
-	public Hashtable<OpDefNode, ValueObj> operatorAssignments;
+	public Map<OpDefNode, ValueObj> operatorAssignments;
 	// def = 1
 
-	private ArrayList<OpDefNode> operatorModelvalues;
+	private List<OpDefNode> operatorModelvalues;
 
-	private final ArrayList<OpDeclNode> bConstantList = new ArrayList<>();
+	private final List<OpDeclNode> bConstantList = new ArrayList<>();
 	// List of constants in the resulting B machine. This list does not contain
 	// a TLA+ constant if the constant is substituted by a modelvalue with the
 	// same name (the constant name is moved to an enumerated set) or if the
 	// constants has arguments and is overridden by an operator
-	public Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
-	// This table contains mappings for operators which are overridden in the
+	public Map<OpDefNode, OpDefNode> operatorOverrideTable;
+	// This map contains mappings for operators which are overridden in the
 	// configuration file
-	public Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
-
-	// This table contains mappings for constants which are overridden in the
+	public Map<OpDeclNode, OpDefNode> constantOverrideTable;
+	// This map contains mappings for constants which are overridden in the
 	// configuration file. All constants with arguments have to be overridden in
 	// the configuration file.
 
@@ -59,13 +58,13 @@ public class ConfigfileEvaluator {
 		this.configAst = configAst;
 		this.moduleNode = moduleNode;
 
-		definitions = new Hashtable<>();
+		definitions = new HashMap<>();
 		OpDefNode[] defs = moduleNode.getOpDefs();
 		for (OpDefNode def : defs) {
 			definitions.put(def.getName().toString(), def);
 		}
 
-		constants = new Hashtable<>();
+		constants = new HashMap<>();
 		OpDeclNode[] cons = moduleNode.getConstantDecls();
 		for (OpDeclNode con : cons) {
 			constants.put(con.getName().toString(), con);
@@ -80,11 +79,11 @@ public class ConfigfileEvaluator {
 	}
 
 	private void initialize() {
-		this.constantOverrideTable = new Hashtable<>();
-		this.operatorOverrideTable = new Hashtable<>();
+		this.constantOverrideTable = new HashMap<>();
+		this.operatorOverrideTable = new HashMap<>();
 
-		this.constantAssignments = new Hashtable<>();
-		this.operatorAssignments = new Hashtable<>();
+		this.constantAssignments = new HashMap<>();
+		this.operatorAssignments = new HashMap<>();
 		this.operatorModelvalues = new ArrayList<>();
 
 		this.enumeratedSet = new ArrayList<>();
@@ -545,35 +544,35 @@ public class ConfigfileEvaluator {
 		return initNode;
 	}
 
-	public Hashtable<OpDeclNode, OpDefNode> getConstantOverrideTable() {
+	public Map<OpDeclNode, OpDefNode> getConstantOverrideTable() {
 		return constantOverrideTable;
 	}
 
-	public ArrayList<OpDefNode> getInvariants() {
+	public List<OpDefNode> getInvariants() {
 		return this.invariantNodeList;
 	}
 
-	public Hashtable<OpDeclNode, ValueObj> getConstantAssignments() {
+	public Map<OpDeclNode, ValueObj> getConstantAssignments() {
 		return this.constantAssignments;
 	}
 
-	public Hashtable<OpDefNode, ValueObj> getOperatorAssignments() {
+	public Map<OpDefNode, ValueObj> getOperatorAssignments() {
 		return this.operatorAssignments;
 	}
 
-	public ArrayList<OpDeclNode> getbConstantList() {
+	public List<OpDeclNode> getbConstantList() {
 		return bConstantList;
 	}
 
-	public Hashtable<OpDefNode, OpDefNode> getOperatorOverrideTable() {
+	public Map<OpDefNode, OpDefNode> getOperatorOverrideTable() {
 		return operatorOverrideTable;
 	}
 
-	public ArrayList<String> getEnumerationSet() {
+	public List<String> getEnumerationSet() {
 		return this.enumeratedSet;
 	}
 
-	public ArrayList<OpDefNode> getOperatorModelvalues() {
+	public List<OpDefNode> getOperatorModelvalues() {
 		return this.operatorModelvalues;
 	}
 }
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index ea9f0887655e3fe8f108059db6e43ee56f2ecece..c9aaf30cdbde8a6f57bb59ca70a854bcbb4735d5 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -3,14 +3,14 @@ package de.tla2b.config;
 import tla2sany.semantic.*;
 import tlc2.tool.BuiltInOPs;
 
-import java.util.Hashtable;
+import java.util.Map;
 
 public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
 
 	private final ModuleNode moduleNode;
-	private final Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
-	private final Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
-	private final Hashtable<OpDefNode, ValueObj> operatorAssignments;
+	private final Map<OpDeclNode, OpDefNode> constantOverrideTable;
+	private final Map<OpDefNode, OpDefNode> operatorOverrideTable;
+	private final Map<OpDefNode, ValueObj> operatorAssignments;
 
 	private ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
 		this.moduleNode = moduleNode;
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index fe94b0ec982bc325f87915b80f1696cb7636eeaf..b0ce020e47eaa237faa3b94d88350ec38958057a 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -4,6 +4,7 @@ import tla2sany.semantic.FrontEnd;
 
 import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.List;
 
 public interface TranslationGlobals {
 	String VERSION_NUMBER = VersionHelper.VERSION;
@@ -26,7 +27,7 @@ public interface TranslationGlobals {
 	String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
 	String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
 
-	ArrayList<String> STANDARD_MODULES = new ArrayList<>(
+	List<String> STANDARD_MODULES = new ArrayList<>(
 		Arrays.asList("Naturals", "FiniteSets", "Integers", "Reals",
 			"Sequences", "TLC", "Relations", "TLA2B", "BBuildIns"));
 }