diff --git a/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
new file mode 100644
index 0000000000000000000000000000000000000000..851fa5938811cd4ecef3bf0160e41489f9bcdfe8
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
@@ -0,0 +1,26 @@
+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public class UnitPragma implements IPragma {
+	private String definedIn;
+	private String attachedTo;
+	private String content;
+
+	public UnitPragma(String definedIn, String attachedTo, String content) {
+		this.definedIn = definedIn;
+		this.attachedTo = attachedTo;
+		this.content = content;
+	}
+
+	@Override
+	public void output(IPrologTermOutput pout) {
+		pout.openTerm("pragma");
+		pout.printAtom("unit");
+		pout.printAtom(definedIn);
+		pout.printAtom(attachedTo);
+		pout.printAtom(content);
+		pout.closeTerm();
+	}
+
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index 62fb49e49dde23f2d56b267667e0184f5c607a6e..bc24a2546a22c0a4f3d60622389b1d623f5a6a8b 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -32,9 +32,11 @@ import org.eventb.core.ISCMachineRoot;
 import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.ITypeEnvironment;
 import org.eventb.core.seqprover.IConfidence;
+import org.rodinp.core.IAttributeType;
 import org.rodinp.core.IRodinElement;
 import org.rodinp.core.IRodinFile;
 import org.rodinp.core.IRodinProject;
+import org.rodinp.core.RodinCore;
 import org.rodinp.core.RodinDBException;
 
 import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma;
@@ -52,8 +54,10 @@ import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.PSet;
 import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.hhu.stups.sablecc.patch.SourcePosition;
+import de.prob.core.internal.Activator;
 import de.prob.core.translator.TranslationFailedException;
 import de.prob.core.translator.pragmas.IPragma;
+import de.prob.core.translator.pragmas.UnitPragma;
 import de.prob.eventb.translator.internal.EProofStatus;
 import de.prob.eventb.translator.internal.ProofObligation;
 import de.prob.eventb.translator.internal.SequentSource;
@@ -112,7 +116,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 				if (rodinFile.exists()) {
 					ISCContextRoot root = (ISCContextRoot) rodinFile.getRoot();
 					collectProofInfo(root);
-					collectPragmas(root);
 				}
 			} catch (Exception e) {
 				// We do not guarantee to include proof infos. If something goes
@@ -124,11 +127,23 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			Assert.isTrue(machine_root.getRodinFile().isConsistent());
 		}
 		translateContext();
-
+		collectPragmas();
 	}
 
-	private void collectPragmas(ISCContextRoot origin) {
-		// TODO
+	private void collectPragmas() throws RodinDBException {
+		// unit pragma, attached to constants
+		final IAttributeType.String UNITATTRIBUTE = RodinCore
+				.getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute");
+
+		final ISCConstant[] constants = context.getSCConstants();
+
+		for (final ISCConstant constant : constants) {
+			if (constant.hasAttribute(UNITATTRIBUTE)) {
+				pragmas.add(new UnitPragma(getResource(), constant
+						.getIdentifierString(), constant
+						.getAttributeValue(UNITATTRIBUTE)));
+			}
+		}
 	}
 
 	private void collectProofInfo(ISCContextRoot origin)
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 fd794beadb03366ee8b2fb99b9a0b8ee16273a51..db29b3ae320fe4d26ef8f30195d9087f80ba93e8 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
@@ -35,13 +35,16 @@ import org.eventb.core.ISCVariable;
 import org.eventb.core.ISCVariant;
 import org.eventb.core.ISCWitness;
 import org.eventb.core.ITraceableElement;
+import org.eventb.core.IVariable;
 import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.ITypeEnvironment;
 import org.eventb.core.ast.Predicate;
 import org.eventb.core.seqprover.IConfidence;
+import org.rodinp.core.IAttributeType;
 import org.rodinp.core.IElementType;
 import org.rodinp.core.IRodinElement;
 import org.rodinp.core.IRodinFile;
+import org.rodinp.core.RodinCore;
 import org.rodinp.core.RodinDBException;
 
 import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus;
@@ -66,8 +69,10 @@ import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.PSubstitution;
 import de.be4.classicalb.core.parser.node.PWitness;
 import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.prob.core.internal.Activator;
 import de.prob.core.translator.TranslationFailedException;
 import de.prob.core.translator.pragmas.IPragma;
+import de.prob.core.translator.pragmas.UnitPragma;
 import de.prob.eventb.translator.AbstractComponentTranslator;
 import de.prob.eventb.translator.AssignmentVisitor;
 import de.prob.eventb.translator.ExpressionVisitor;
@@ -176,8 +181,20 @@ public class ModelTranslator extends AbstractComponentTranslator {
 		collectPragmas();
 	}
 
-	private void collectPragmas() {
-		// TODO
+	private void collectPragmas() throws RodinDBException {
+		// unit pragma, attached to constants
+		final IAttributeType.String UNITATTRIBUTE = RodinCore
+				.getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute");
+
+		final IVariable[] variables = origin.getVariables();
+
+		for (final IVariable variable : variables) {
+			if (variable.hasAttribute(UNITATTRIBUTE)) {
+				pragmas.add(new UnitPragma(getResource(), variable
+						.getIdentifierString(), variable
+						.getAttributeValue(UNITATTRIBUTE)));
+			}
+		}
 	}
 
 	private void collectProofInfo() throws RodinDBException {
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
index 3b2ce2fef1afabc5548adb7680b35f0e0ee987d4..4bbe282bcfb7ed929ee4e66951746ad85f7954c2 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -56,7 +56,7 @@ import de.prob.parser.ResultParserException;
 import de.prob.prolog.term.CompoundPrologTerm;
 import de.prob.prolog.term.ListPrologTerm;
 import de.prob.prolog.term.PrologTerm;
-import de.prob.ui.pragmas.InferredUnitPragma;
+import de.prob.ui.pragmas.InferredUnitPragmaAttribute;
 
 public class StartUnitAnalysisHandler extends AbstractHandler implements
 		IHandler {
@@ -178,7 +178,8 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 					for (IVariable var : allVariables) {
 						String variableName = var.getIdentifierString();
 						if (variables.containsKey(variableName)) {
-							var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+							var.setAttributeValue(
+									InferredUnitPragmaAttribute.ATTRIBUTE,
 									variables.get(variableName),
 									new NullProgressMonitor());
 						}
@@ -192,7 +193,8 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 					for (IConstant var : allConstants) {
 						String constantName = var.getIdentifierString();
 						if (variables.containsKey(constantName)) {
-							var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+							var.setAttributeValue(
+									InferredUnitPragmaAttribute.ATTRIBUTE,
 									variables.get(constantName),
 									new NullProgressMonitor());
 						}