diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index c2821088de12e65204dc7948af9a1ec40f751904..e0652e807354e890a50e81e86c746be0329b8252 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -35,6 +35,18 @@ public class BBuiltInsTest {
 		assertEquals("POW(BOOL)", t.getConstantType("k"));
 	}
 
+	@Test
+	public void testNestedBooleanDefinitions() throws Exception {
+		String module = "---- MODULE Testing ----\n"
+				+ "EXTENDS Naturals \n"
+				+ "InnerDef(b) == b>5 \n"
+				+ "HelpDef(a,b) == a<7 /\\ InnerDef(b) \n"
+				+ "Init == TRUE = HelpDef(3,4) \n"
+				+ "===============";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("BOOL", t.getDefinitionType("HelpDef"));
+		assertEquals("BOOL", t.getDefinitionType("InnerDef"));
+	}
 
 	/*
 	 * String