diff --git a/src/main/resources/standardModules/Functions.tla b/src/main/resources/standardModules/Functions.tla
index 7e9d2bb4e7f2054773d7a20c30d1b5ee8040373b..6cffb418835599804399a1503ac4cb4fecb9fafc 100644
--- a/src/main/resources/standardModules/Functions.tla
+++ b/src/main/resources/standardModules/Functions.tla
@@ -1,5 +1,5 @@
 ----------------------------- MODULE Functions -----------------------------
-EXTENDS FiniteSets
+EXTENDS FiniteSets, TLC
 
 Range(f) == {f[x] : x \in DOMAIN f}
  \* The range of the function f
@@ -31,7 +31,8 @@ Inverse(f) == {<<f[x],x>>: x \in DOMAIN f}
 Override(f, g) == [x \in (DOMAIN f) \cup DOMAIN g |-> IF x \in DOMAIN g THEN g[x] ELSE f[x]]
  \* Overwriting of the function f with the function g
 
-FuncAssign(f, d, e) == [f EXCEPT ![d] = e]
+FuncAssign(f, d, e) ==  d :> e @@ f
+ \* [x \in (DOMAIN f) \cup {d} |-> IF x = d THEN e ELSE f[x]]
  \* Overwriting the function f at index d with value e
 
 TotalInjFunc(S, T) == {f \in [S -> T]:
diff --git a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
new file mode 100644
index 0000000000000000000000000000000000000000..90a830910e8328eca53fd4749b8733d91fac0e3c
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
@@ -0,0 +1,23 @@
+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+
+public class FixedBugs {
+
+	@Test
+	public void testFunctionAssignment() throws Exception {
+		String machine = 
+				"MACHINE Test\n"
+				+ "VARIABLES x \n"
+				+ "INVARIANT x : 1..3 +-> 1..2 \n"
+				+ "INITIALISATION x := {} \n"
+				+ "OPERATIONS foo = PRE x = {} THEN x(1) := 2 END \n"
+				+ "END";
+		assertEquals(Deadlock, testString(machine));
+	}
+}