diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 106d7b7ad7e2726f4b9c0db615af6b95e1ee6f5d..f8e094572c84923d751cd7312b18ccf6574126bf 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -64,7 +64,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 				.getModuleNode().getVariableDecls()));
 
 		evalParams();
+		// System.out.println("Construction B Operation for TLA+ action: " + name);
 		findUnchangedVariables();
+		// System.out.println(" UNCHANGED = " + unchangedVariables.toString());
 		separateGuardsAndBeforeAfterPredicates(node);
 		findAssignments();
 	}
@@ -186,19 +188,22 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 
 					if (OPCODE_eq == getOpCode(opApplNode.getOperator()
 							.getName())) {
-						ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
+						ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; // we have equality arg1 = RHS
 						try {
 							OpApplNode arg11 = (OpApplNode) arg1;
 							if (getOpCode(arg11.getOperator().getName()) == OPCODE_prime) {
 								OpApplNode v = (OpApplNode) arg11.getArgs()[0];
 								SymbolNode var = v.getOperator();
+								// we have equality var' = RHS
 								if (!primedVariablesFinder
 										.getTwiceUsedVariables().contains(var)) {
-									// var is only used once in all before after
-									// predicates
+									// var' is only used once in all before after predicates
+									// meaning we do not need it as parameter of the ANY
+									// and can add an assignment var := RHS
 									assignments.put(v.getOperator(),
-											opApplNode.getArgs()[1]);
+											opApplNode.getArgs()[1]); // RHS of assignment
 									beforeAfterPredicates.remove(node);
+								    // System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>");
 								}
 
 							}
@@ -241,8 +246,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 					return;
 				}
 				default: {
-					if (opApplNode.level < 2) {
-						guards.add(node);
+					if (opApplNode.level < 2) {  
+						guards.add(node); // should we be checking nonLeibnizParams is empty ?
 						return;
 					} else {
 						beforeAfterPredicates.add(node);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 8fd68c51165e6f64439e3c02abda855ebdef76cd..663673fb66fcdaf0d6348d39d22adb85f3195223 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2186,8 +2186,8 @@ public class BAstCreator extends BuiltInOPs
 			break;
 		}
 		case OPCODE_unchanged: {
-			// System.out.println("hier");
 			OpApplNode node = (OpApplNode) n.getArgs()[0];
+			// System.out.println(" Translating UNCHANGED : " + node.toString());
 			if (node.getOperator().getKind() == VariableDeclKind) {
 				AEqualPredicate equal = new AEqualPredicate();
 				equal.setLeft(createIdentifierNode(getName(node.getOperator()) + "_n"));