diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 6fa6a8b47ac08698bf2608561652f079609c2b60..0d134ea603da87ab1a6a97ebbc698dc4b2483443 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -115,4 +115,17 @@ public class TestModuleNaturals {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testNestedDefinitions() throws Exception {
+		String module = "---- MODULE Testing ----\n"
+				+ "EXTENDS Naturals \n"
+				+ "InnerDef(b) == b*5 \n"
+				+ "HelpDef(a,b) == a+b \n"
+				+ "Init == 1 = HelpDef(1,1) \n"
+				+ "===============";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("INTEGER", t.getDefinitionType("HelpDef"));
+		assertEquals("INTEGER", t.getDefinitionType("InnerDef"));
+	}
+
 }
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index 4ba3f0ed7a579be5d7377f97dcd717f7604ac5f3..8b4cf347248df34010cc6728515f6204148a9fd2 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -4,11 +4,11 @@ import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.exceptions.TypeErrorException;
 import de.tla2b.util.TestTypeChecker;
 import de.tla2b.util.TestUtil;
+import org.junit.Ignore;
 import org.junit.Test;
 
 import static org.junit.Assert.assertEquals;
 
-
 public class TestModuleReals {
 
 	/*
@@ -172,4 +172,19 @@ public class TestModuleReals {
 			+ "=================================";
 		TestUtil.typeCheckString(module);
 	}
+
+	@Ignore
+	@Test
+	public void testNestedDefinitions() throws Exception {
+		// FIXME: this fails because the default type is Int and we first type everything as Int
+		String module = "---- MODULE Testing ----\n"
+				+ "EXTENDS Reals \n"
+				+ "InnerDef(b) == b*5.0 \n"
+				+ "HelpDef(a,b) == a+InnerDef(b) \n"
+				+ "Init == 1.0 = HelpDef(1.0,1.0) \n"
+				+ "===============";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("REAL", t.getDefinitionType("HelpDef"));
+		assertEquals("REAL", t.getDefinitionType("InnerDef"));
+	}
 }