diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index cf28ac6e2ec6d59b4fad908d5219fde92aef2c25..949138d92f0defb7f10a33a4a26e945b38db5f6f 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -2,6 +2,7 @@ package de.tla2b.translation;
 
 import java.util.ArrayList;
 import java.util.HashSet;
+import java.util.Set;
 
 import tla2sany.semantic.ASTConstants;
 import tla2sany.semantic.AssumeNode;
@@ -49,11 +50,6 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
 			bDefinitionsSet.add(def);
 		}
 
-		HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
-		for (OpDefNode opDefNode : temp) {
-			visitExprNode(opDefNode.getBody());
-		}
-
 		for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
 			String defName = opDef.getName().toString();
 			// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx,
@@ -62,11 +58,19 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
 				bDefinitionsSet.add(opDef);
 			}
 		}
+
+		HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
+		for (OpDefNode opDefNode : temp) {
+			visitExprNode(opDefNode.getBody());
+		}
+
 	}
 
+	@Override
 	public void visitUserDefinedNode(OpApplNode n) {
 		OpDefNode def = (OpDefNode) n.getOperator();
 		if (bDefinitionsSet.add(def)) {
+			// visit body only once
 			visitExprNode(def.getBody());
 		}
 		for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
@@ -74,7 +78,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
 		}
 	}
 
-	public HashSet<OpDefNode> getBDefinitionsSet() {
+	public Set<OpDefNode> getBDefinitionsSet() {
 		return bDefinitionsSet;
 	}