diff --git a/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java
index ed7fccdd4d3..3e958126829 100644
--- a/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java
+++ b/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java
@@ -214,7 +214,7 @@ private List<KVariable> closure(K k) {
     List<KVariable> result = new ArrayList<>();
     new GatherVarsVisitor(true, errors, vars, false).apply(k);
     new ComputeUnboundVariables(true, true, errors, vars, result::add).apply(k);
-    return result;
+    return result.stream().distinct().collect(Collectors.toList());
   }
 
   private Production funProd(KLabel fun, K k, Sort arg, boolean total) {