diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 64358c17e6927110c1b8770b6a9ef90535918ab5..48653e2efd103a878378efe94911d35cc53dfe5f 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -9,6 +9,7 @@ import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
 import java.util.LinkedList;
+import java.util.List;
 import java.util.Set;
 import java.util.Map.Entry;
 
@@ -331,7 +332,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at '@',%n%s ", expected, type,
 						exprNode.getLocation()));
 			}
-			
 
 		}
 
@@ -358,14 +358,17 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 
 	}
 
-	private void setType(SemanticNode node, TLAType type){
+	private void setType(SemanticNode node, TLAType type) {
 		node.setToolObject(TYPE_ID, type);
-		if (type instanceof AbstractHasFollowers){
+		if (type instanceof AbstractHasFollowers) {
 			((AbstractHasFollowers) type).addFollower(node);
 		}
 	}
-	
-	
+
+	private TLAType getType(OpApplNode n) {
+		return (TLAType) n.getToolObject(TYPE_ID);
+	}
+
 	/**
 	 * @param n
 	 * @param expected
@@ -431,8 +434,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			if (t == null) {
 				t = (TLAType) symbolNode.getToolObject(TYPE_ID);
 			}
-			
-			if(t == null){
+
+			if (t == null) {
 				throw new RuntimeException();
 			}
 			try {
@@ -458,10 +461,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			}
 
 			TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
-			if (found == null)
+			if (found == null){
 				found = new UntypedType();
 			// throw new RuntimeException(def.getName() + " has no type yet!");
-			found = found.cloneTLAType();
+			}
+			if(n.getArgs().length != 0){
+				found = found.cloneTLAType();
+			}
+			
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -867,8 +874,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 					n.getArgs()[0].setToolObject(TYPE_ID, res);
 					tupleNodeList.add(n.getArgs()[0]);
 					if (res instanceof AbstractHasFollowers) {
-						((AbstractHasFollowers) res).addFollower(n
-								.getArgs()[0]);
+						((AbstractHasFollowers) res)
+								.addFollower(n.getArgs()[0]);
 					}
 					TLAType found = (TLAType) n.getToolObject(TYPE_ID);
 					try {
@@ -1069,14 +1076,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		}
 
 		case OPCODE_uc: {
-			TLAType found = new UntypedType();
-			FormalParamNode x = n.getUnbdedQuantSymbols()[0];
-			symbolNodeList.add(x);
-			x.setToolObject(TYPE_ID, found);
-			((AbstractHasFollowers) found).addFollower(x);
-			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
-
-			found = (TLAType) x.getToolObject(TYPE_ID);
+			List<TLAType> list = new ArrayList<TLAType>();
+			for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
+				TLAType paramType = new UntypedType();
+				symbolNodeList.add(param);
+				setType(param, paramType);
+				list.add(paramType);
+			}
+			TLAType found = null;
+			if (list.size() == 1) {
+				found = list.get(0);
+			} else {
+				found = new TupleType(list);
+			}
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -1084,20 +1096,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at 'CHOOSE',%n%s", expected,
 						found, n.getLocation()));
 			}
-			return found;
+			setType(n, found);
+			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+
+			return getType(n);
+
 		}
 
 		case OPCODE_bc: { // CHOOSE x \in S: P
-			if (n.isBdedQuantATuple()[0]) {
-				throw new TypeErrorException(
-						"A tuple as parameter within the set constructor is not permitted.\n"
-								+ n.getLocation());
-			}
-			ExprNode[] bounds = n.getBdedQuantBounds();
-			SetType S = (SetType) visitExprNode(bounds[0], new SetType(
-					new UntypedType()));
-			TLAType found = S.getSubType();
-
+			TLAType found = evalBoundedVariables(n);
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -1105,12 +1112,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at 'CHOOSE',%n%s", expected,
 						found, n.getLocation()));
 			}
-			FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
-			symbolNodeList.add(x);
-			x.setToolObject(TYPE_ID, found);
-			if (found instanceof AbstractHasFollowers) {
-				((AbstractHasFollowers) found).addFollower(x);
-			}
 			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
 			return found;
 		}
@@ -1205,8 +1206,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		return domType;
 	}
 
-	
-	
 	/**
 	 * @param n
 	 * @param expected
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 106aa3ed20617d64b8a3955e4c936ce3932675d2..31c2924d0d31f95c3f1ba4213c6008ca0668c922 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2020,8 +2020,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		ADefinitionExpression defCall = new ADefinitionExpression();
 		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
 		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
-		FormalParamNode x = n.getUnbdedQuantSymbols()[0];
-		comprehension.setIdentifiers(createIdentifierList(getName(x)));
+		List<PExpression> paramList = new ArrayList<PExpression>();
+		for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
+			paramList.add(createIdentifierNode(param));
+		}
+		comprehension.setIdentifiers(paramList);
 		comprehension
 				.setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
 		List<PExpression> list = new ArrayList<PExpression>();
@@ -2034,14 +2037,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		ADefinitionExpression defCall = new ADefinitionExpression();
 		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
 		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
-		FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
-		comprehension.setIdentifiers(createIdentifierList(x));
-		AMemberPredicate member = new AMemberPredicate();
-		member.setLeft(createIdentifierNode(x));
-		ExprNode in = n.getBdedQuantBounds()[0];
-		member.setRight(visitExprNodeExpression(in));
+		List<PExpression> paramList = new ArrayList<PExpression>();
+		for (FormalParamNode param : n.getBdedQuantSymbolLists()[0]) {
+			paramList.add(createIdentifierNode(param));
+		}
+		comprehension.setIdentifiers(paramList);
+		PPredicate typingPredicate = visitBoundsOfLocalVariables(n);
 		AConjunctPredicate conj = new AConjunctPredicate();
-		conj.setLeft(member);
+		conj.setLeft(typingPredicate);
 		conj.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
 		comprehension.setPredicates(conj);
 		List<PExpression> list = new ArrayList<PExpression>();
diff --git a/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java
index 366bb0a4a8b3b4a730f50dfe4c22bd4418ce0c4c..2b5b32d28220e63b7494ff31ee446341ded71941 100644
--- a/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java
@@ -131,6 +131,21 @@ public class MiscellaneousConstructsTest {
 		compare(expected, module);
 	}
 	
+
+	
+	@Test
+	public void testUnBoundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) : {(1,TRUE)} & TRUE = TRUE}) \n" + "END";
+		compare(expected, module);
+	}
+	
+	
 	@Test
 	public void testBoundedChoosePredicate() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -142,4 +157,28 @@ public class MiscellaneousConstructsTest {
 				+ "PROPERTIES CHOOSE({x | x : {TRUE} & TRUE = TRUE}) = TRUE \n" + "END";
 		compare(expected, module);
 	}
+	
+	@Test
+	public void testBoundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) : {(1,TRUE)} & TRUE = TRUE}) \n" + "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testUnboundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> : <<a,b>> = <<1,TRUE>>\n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) = (1,TRUE)}) \n" + "END";
+		compare(expected, module);
+	}
 }
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index 2f7eca3453789bb66b9e5e5b38cd705417a547e1..78be1a2f71ad09f1c954247909bef0f3819d1cca 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -141,6 +141,23 @@ public class TupleTest {
 		compare(expected, module);
 	}
 	
+	@Ignore
+	@Test
+	public void testAtTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k =[i \\in Nat |-> <<1, \"s\">>] /\\ k2 = [ k EXCEPT ![22] = <<@[1],\"d\">>] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "CONSTANTS k, k2 \n"
+				+ "PROPERTIES \n"
+				+ "(k : INTEGER +-> INTEGER * STRING & k2 : INTEGER +-> INTEGER * STRING)"
+				+ " & (k = %(i).(i : NATURAL | (1,\"s\")) & k2 = k <+ {(22,( prj1(INTEGER,STRING)(k(22)),\"d\") )}) \n"
+				+ "END";
+		compare(expected, module);
+	}
 	
 	
 }
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index e5984d3845291052e433630713178443c3021bd9..82d4cc18787154a905a01807280971467fd5b200 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -122,7 +122,7 @@ public class ExceptTest {
 	}
 	
 	@Test
-	public void testRecordTest() throws Exception {
+	public void testRecordExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 				+ "EXTENDS Naturals \n"
 				+ "CONSTANTS k\n"
@@ -132,5 +132,19 @@ public class ExceptTest {
 		TestTypeChecker t = TestUtil.typeCheckString(module);
 		assertEquals("INTEGER", t.getConstantType("k"));
 	}
+	
+	@Test
+	public void testAtTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k, k2\n"
+				+ "ASSUME k  = [i \\in Nat |-> <<1, \"s\">>] /\\ k2 = [ k EXCEPT ![22] = <<@[1],\"d\">>] \n"
+				+ "=================================";
+
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(INTEGER*(INTEGER*STRING))", t.getConstantType("k"));
+		assertEquals("POW(INTEGER*(INTEGER*STRING))", t.getConstantType("k2"));
+	}
+	
 
 }
diff --git a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
index 38b627a7299d29f6670e34518b1c2ea8672c52bd..e49d769afedfc53d0c910852f4ffaaa7d53bcf03 100644
--- a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
@@ -105,5 +105,45 @@ public class MiscellaneousConstructsTest {
 		assertEquals("BOOL",t.getConstantType("k4"));
 	}
 	
+	@Test
+	public void testBoundedChoose() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE x \\in {1}: TRUE  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testUnboundedChoose() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE x : x = 1  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testUnboundedChooseTuple() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE <<a,b>> : <<a,b>> = <<1,TRUE>>  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*BOOL",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testBoundedChooseTuple() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*BOOL",t.getConstantType("k"));
+	}
+	
 	
 }
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index ddd967e513aa8510928ec1e3dd253ecd06924f02..e9ef27613053e7aa38d4797092f30d681f2de88e 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -6,7 +6,6 @@ package de.tla2b.typechecking;
 
 import static org.junit.Assert.assertEquals;
 
-import org.junit.Ignore;
 import org.junit.Test;
 
 import de.tla2b.exceptions.FrontEndException;