diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 5197cbb1fd4bd66d02468933d7776baacb716da0..0486e12b8d88b4b6bca8c7efef9e6c873b2f6bde 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -105,6 +105,7 @@ import de.be4.classicalb.core.parser.node.AStringExpression;
 import de.be4.classicalb.core.parser.node.AStringSetExpression;
 import de.be4.classicalb.core.parser.node.AStructExpression;
 import de.be4.classicalb.core.parser.node.ASubsetPredicate;
+import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.ATailExpression;
 import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
 import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
@@ -271,16 +272,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			}
 
 		}
-		Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
-				.getUsedExternalFunctions();
 
-		if (bDefs.size() == 0 && set.size() == 0) {
-			return;
-		}
-
-		ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
 		List<PDefinition> defs = new ArrayList<PDefinition>();
 
+		Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
+				.getUsedExternalFunctions();
 		defs.addAll(createDefinitionsForExternalFunctions(set));
 
 		for (OpDefNode opDefNode : bDefs) {
@@ -299,7 +295,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				d.setParameters(list);
 				d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
 				defs.add(d);
-				bDefinitions.addDefinition(d, Definitions.Type.Expression);
 			} else {
 				AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
 				d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
@@ -307,12 +302,31 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				d.setParameters(list);
 				d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
 				defs.add(d);
-				bDefinitions.addDefinition(d, Definitions.Type.Expression);
 			}
 
 		}
-		defClause.setDefinitions(defs);
-		machineClauseList.add(defClause);
+
+		if (defs.size() > 0) {
+			ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
+			defClause.setDefinitions(defs);
+			machineClauseList.add(defClause);
+			for (PDefinition def : defs) {
+				if (def instanceof AExpressionDefinitionDefinition) {
+					bDefinitions.addDefinition(
+							(AExpressionDefinitionDefinition) def,
+							Definitions.Type.Expression);
+				} else if (def instanceof APredicateDefinitionDefinition) {
+					bDefinitions.addDefinition(
+							(APredicateDefinitionDefinition) def,
+							Definitions.Type.Predicate);
+				} else {
+					bDefinitions.addDefinition(
+							(ASubstitutionDefinitionDefinition) def,
+							Definitions.Type.Substitution);
+				}
+			}
+		}
+
 	}
 
 	private ArrayList<PDefinition> createDefinitionsForExternalFunctions(
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index c16b5747497aa0aba28df170167f693c686a00c6..6546b278f7647879fd70eb04fd463c0e25faa749 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -210,7 +210,6 @@ public class Translator {
 				specAnalyser, usedExternalFunctions, predicateVsExpression);
 
 		this.bDefinitions = bAstCreator.getBDefinitions();
-
 		return bAstCreator.getStartNode();
 	}
 
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index 19d068fdb4842ba123ed187904d6507a2b3a8d5b..f8bad910022269da67bf7241cb8065f99e16d4da 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -55,6 +55,7 @@ public class MCTest {
 		runModule(file);
 	}
 	
+	
 	@Test
 	public void testChannel() throws Exception {
 		String file = "src/test/resources/examples/Channel/Channel.tla";