diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 1a5ac15125014e0d0f39d01c19e6d3bab2f29766..f758cebad3f5989f5ec1fcbd89f7933804ad46bb 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -395,8 +395,6 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
 				}else{
 					throw new RuntimeException(vName + " has no type yet!");
 				}
-				
-				
 			}
 			try {
 				TLAType result = expected.unify(v);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index cd10aed527fc9c81c775bac7f17d9eff1448f6db..80b2bda6c3a8055001dd0cac65c65a5386bdfc3e 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2,7 +2,6 @@ package de.tla2bAst;
 
 import java.util.ArrayList;
 import java.util.Arrays;
-import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
 import java.util.LinkedList;
@@ -182,8 +181,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		this.specAnalyser = specAnalyser;
 		this.bMacroHandler = new BMacroHandler();
 		this.predicateVsExpression = new PredicateVsExpression(moduleNode);
-		this.recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
-		
+		this.recursiveFunctionHandler = new RecursiveFunctionHandler(
+				specAnalyser);
+
 		ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
 				.getBody();
 		AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
@@ -289,6 +289,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 								.containsValue(def)) {
 					continue;
 				}
+				if (def.getOriginallyDefinedInModuleNode().getName().toString()
+						.equals("MC")) {
+					continue;
+				}
+
 				bDefs.add(def);
 			}
 
@@ -695,8 +700,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 	private void createInvariantClause() {
 		OpDeclNode[] vars = moduleNode.getVariableDecls();
-		if (vars.length == 0)
-			return;
 
 		List<PPredicate> predList = new ArrayList<PPredicate>();
 		for (int i = 0; i < vars.length; i++) {
@@ -711,15 +714,23 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 		if (conEval != null) {
 			for (OpDefNode def : conEval.getInvariants()) {
-				ADefinitionPredicate defPred = new ADefinitionPredicate();
-				defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
-				predList.add(defPred);
+				if (def.getOriginallyDefinedInModuleNode().getName().toString()
+						.equals("MC")) {
+					predList.add(visitExprNodePredicate(def.getBody()));
+				} else {
+					ADefinitionPredicate defPred = new ADefinitionPredicate();
+					defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
+					predList.add(defPred);
+				}
 			}
 		}
 
-		AInvariantMachineClause invClause = new AInvariantMachineClause(
-				createConjunction(predList));
-		machineClauseList.add(invClause);
+		if (predList.size() > 0) {
+			AInvariantMachineClause invClause = new AInvariantMachineClause(
+					createConjunction(predList));
+			machineClauseList.add(invClause);
+		}
+
 	}
 
 	private PPredicate visitAssumeNode(AssumeNode assumeNode) {
diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
index f2d2e42a7692eb1b12a0ce6c7cbec0ed84ae4136..449e378b48dfc042fb5c90640f458a7dd9a0c1f2 100644
--- a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
@@ -20,4 +20,4 @@ public class ModuleAndExpressionTest {
 				+ "ASSUME k = 4" + "===============";
 		compareExprIncludingModel(null, "k = TRUE", module);
 	}
-}
+}
\ No newline at end of file
diff --git a/src/test/resources/regression/Club/Club_tla.mch b/src/test/resources/regression/Club/Club_tla.mch
deleted file mode 100644
index 48809d63bb87ddbfb14d10a01ebebf875dc05eab..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/Club/Club_tla.mch
+++ /dev/null
@@ -1,18 +0,0 @@
-/*@ generated by TLA2B 1.0.7 Fri May 09 16:29:56 CEST 2014 */
-MACHINE Club
-SETS ENUM1 = {n1, n2, n3}
-ABSTRACT_CONSTANTS capacity, NAME, total
-PROPERTIES
-((((capacity : INTEGER & NAME = ENUM1) & total : INTEGER) & (capacity : NATURAL & capacity = 2)) & card(NAME) > capacity) & (total : NATURAL & total > 2)
-VARIABLES member, waiting
-INVARIANT
-member : POW(ENUM1) & waiting : POW(ENUM1)
-INITIALISATION
-member, waiting:(member = {} & waiting = {})
-OPERATIONS
- join_queue(nn) = ANY member_n WHERE ((((nn : NAME & nn /: member) & nn /: waiting) & member_n : POW(ENUM1)) & card(waiting) < total) & member_n = member THEN waiting,member := waiting \/ {nn},member_n END;
-
- join(nn) = SELECT ((nn : NAME & nn : waiting) & card(member) < capacity) & card(member) < capacity THEN member,waiting := member \/ {nn},waiting - {nn} END;
-
- remove(nn) = ANY waiting_n WHERE ((nn : NAME & nn : member) & waiting_n : POW(ENUM1)) & waiting_n = waiting THEN member,waiting := member - {nn},waiting_n END
-END
\ No newline at end of file