diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index b3528e59ecb5ccb40a1686ba07a1bc0e897db618..1f92618a63a947c0ce8cbff336689a6c3657a706 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -723,23 +723,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			for (int j = 0; j < seq.getArgs().length; j++) {
 				list.add(seq.getArgs()[j]);
 			}
-			if (type instanceof FunctionType) {
+			PExpression base = visitExprNodeExpression(at.getAtBase());
+			return evalAtNode(list, type, base);
 
-				List<PExpression> params = new ArrayList<PExpression>();
-				params.add(visitExprOrOpArgNodeExpression(list.get(0)));
-
-				AFunctionExpression funCall = new AFunctionExpression();
-				funCall.setIdentifier(visitExprNodeExpression(at.getAtBase()));
-				funCall.setParameters(params);
-				return funCall;
-			} else {
-				ARecordFieldExpression select = new ARecordFieldExpression();
-				select.setRecord(visitExprNodeExpression(at.getAtBase()));
-				StringNode stringNode = (StringNode) list.get(0);
-				select.setIdentifier(createIdentifierNode(stringNode.getRep()
-						.toString())); // TODO renamed
-				return select;
-			}
 		}
 
 		case LetInKind: {
@@ -752,6 +738,33 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		throw new RuntimeException(n.getClass().toString());
 	}
 
+	private PExpression evalAtNode(LinkedList<ExprOrOpArgNode> list,
+			TLAType type, PExpression base) {
+		if(list.size() == 0){
+			return base;
+		}
+		
+		if (type instanceof FunctionType) {
+			FunctionType funcType = (FunctionType) type;
+			PExpression param = visitExprOrOpArgNodeExpression(list.poll());
+			List<PExpression> params = new ArrayList<PExpression>();
+			params.add(param);
+
+			AFunctionExpression funCall = new AFunctionExpression();
+			funCall.setIdentifier(base);
+			funCall.setParameters(params);
+			return evalAtNode(list, funcType.getRange(), funCall);
+		} else {
+			StructType structType = (StructType) type;
+			ARecordFieldExpression select = new ARecordFieldExpression();
+			select.setRecord(base);
+			StringNode stringNode = (StringNode) list.poll();
+			String fieldName = stringNode.getRep().toString();
+			select.setIdentifier(createIdentifierNode(fieldName)); // TODO renamed
+			return evalAtNode(list, structType.getType(fieldName), select);
+		}
+	}
+
 	private PPredicate visitOpApplNodePredicate(OpApplNode n) {
 		switch (n.getOperator().getKind()) {
 		case VariableDeclKind:
@@ -1453,7 +1466,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			if (t != null && t instanceof TupleType) {
 				NumeralNode num = (NumeralNode) n.getArgs()[1];
 				int field = num.val();
-				System.out.println(t);
 				return createProjectionFunction(n, field, t);
 			} else {
 				AFunctionExpression func = new AFunctionExpression();
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
index ddd109cd01d6bc8181348010fcd847725f70ee27..790abffee29ca941a5d94a5c3613e68270466e8a 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -22,6 +22,35 @@ public class ExceptTest {
 		compare(expected, module);
 	}
 
+	@Test
+	public void testFunctionAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |-> i] /\\ k # [k EXCEPT ![3] = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES " 
+				+ "k : INTEGER +-> INTEGER & (k = %(i).(i : {3, 4} | i) & k /= k <+ {(3,k(3) + 1)}) \n" 
+				+ "END";
+		compare(expected, module);
+	}
+	@Test
+	public void testNestedFunctionAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {TRUE} |-> <<5,6>>] /\\ k # [k EXCEPT ![TRUE][2] = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES " 
+				+ "k : BOOL +-> (INTEGER +-> INTEGER) & (k = %(i).(i : {TRUE} | [5,6]) & k /= k <+ {(TRUE,k(TRUE) <+ {(2,(k(TRUE))(2) + 1)})}) \n" 
+				+ "END";
+		compare(expected, module);
+	}
+	
 	@Test
 	public void testRecordExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -37,6 +66,38 @@ public class ExceptTest {
 
 	}
 	
+	@Test
+	public void testRecordAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k /= [k EXCEPT !.a = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:k'a + 1, b:k'b)) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
+	@Test
+	public void testNestedRecordAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> [b |-> 1]] /\\ k /= [k EXCEPT !.a.b = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : struct(a:struct(b:INTEGER)) & (k = rec(a:rec(b:1)) & k /= rec(a:rec(b:(k'a)'b + 1))) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
 	@Test
 	public void testRecordFunctionExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -52,6 +113,22 @@ public class ExceptTest {
 
 	}
 	
+	@Test
+	public void testRecordFunctionAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> <<3>>] /\\ k /= [k EXCEPT !.a[1] = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : struct(a:INTEGER +-> INTEGER) & (k = rec(a:[3]) & k /= rec(a:k'a <+ {(1,(k'a)(1) + 1)})) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
 	@Test
 	public void testFunctionRecordExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -67,6 +144,22 @@ public class ExceptTest {
 
 	}
 	
+	@Test
+	public void testFunctionRecordAt() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |->[a |-> i, b |-> TRUE ] ] /\\ k /= [k EXCEPT ![3].a = @ + 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : INTEGER +-> struct(a:INTEGER, b:BOOL) & (k = %(i).(i : {3, 4} | rec(a:i, b:TRUE)) & k /= k <+ {(3,rec(a:k(3)'a + 1, b:k(3)'b))}) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
 	@Test
 	public void testRecordExceptNested() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"