diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index 45049f26186f142fef8e614154bf1e2a32fc1c6c..35069296df203760aeb10595d0de2a9b989f9716 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -36,6 +36,8 @@ import org.eventb.core.ISCWitness;
 import org.eventb.core.ITraceableElement;
 import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.basis.Event;
+import org.eventb.core.basis.Guard;
 import org.eventb.core.seqprover.IConfidence;
 import org.rodinp.core.IElementType;
 import org.rodinp.core.IRodinElement;
@@ -135,9 +137,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
 		super(machine.getComponentName());
 		this.machine = machine;
 		origin = machine.getMachineRoot();
-		ff = ((ISCMachineRoot) machine).getFormulaFactory();
+		ff = machine.getFormulaFactory();
 		try {
-			te = ((ISCMachineRoot) machine).getTypeEnvironment(ff);
+			te = machine.getTypeEnvironment(ff);
 		} catch (RodinDBException e) {
 			final String message = "A Rodin exception occured during translation process. Original Exception: ";
 			throw new TranslationFailedException(machine.getComponentName(),
@@ -208,6 +210,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
 						.getElementType();
 				s.add(new SequentSource(type, le.getLabel()));
 
+				if (srcElement instanceof Guard) {
+					Event srcEvent = (Event) srcElement.getParent();
+					String srvEventName = srcEvent.getLabel();
+					s.add(new SequentSource(srcEvent.getElementType(),
+							srvEventName));
+				}
+
 			}
 			addProof(new ProofObligation(origin, s, name, pstatus));
 		}