fix bug in previous commit

ykzeng · Aug 16, 2013 · 3bfde4e · 3bfde4e
1 parent e59337f
commit 3bfde4e
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/javasources/KTool/src/org/kframework/kil/Production.java b/javasources/KTool/src/org/kframework/kil/Production.java
@@ -232,7 +232,12 @@ public boolean equals(Object obj) {
 			if (!prd.getItems().get(i).equals(items.get(i)))
 				return false;
 		}
-        if (!prd.getAttributes().get("klabel").equals(getAttributes().get("klabel"))) {
+        String klabel1 = prd.getAttributes().get("klabel");
+        String klabel2 = getAttributes().get("klabel");
+        if ((klabel1 == null && klabel2 != null) || (klabel1 != null && klabel2 == null)) {
+            return false;
+        }
+        if (klabel1 != null && klabel2 != null && klabel1.equals(klabel2)) {
             return false;
         }
 		return true;