diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
index af73562e97..ef9711826e 100644
--- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
+++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -298,7 +298,7 @@ public void convert(
       if (isFunction(prod) && prod.att().contains(Att.UNIT())) {
         genUnitAxiom(prod, semantics);
       }
-      if (isFunctional(prod, functionRules)) {
+      if (isFunctional(prod)) {
         genFunctionalAxiom(prod, semantics);
       }
       if (isConstructor(prod, functionRules)) {
@@ -458,7 +458,7 @@ private void translateSymbol(
       Production prod,
       StringBuilder sb) {
     sb.append("  ");
-    if (isFunction(prod) && prod.att().contains(Att.HOOK()) && isRealHook(prod.att())) {
+    if (isFunction(prod) && isHook(prod)) {
       sb.append("hooked-");
     }
     sb.append("symbol ");
@@ -475,7 +475,7 @@ private void translateSymbol(
     sb.append(") : ");
     convert(prod.sort(), prod, sb);
     sb.append(" ");
-    Att koreAtt = addKoreAttributes(prod, functionRules, overloads);
+    Att koreAtt = koreAttributes(prod, functionRules, overloads);
     convert(attributes, koreAtt, sb, null, null);
     sb.append("\n");
   }
@@ -930,16 +930,6 @@ private void genOverloadedAxiom(Production lesser, Production greater, StringBui
     sb.append(" // overloaded production\n");
   }
 
-  private boolean isRealHook(Att att) {
-    String hook = att.get(Att.HOOK());
-    return Stream.concat(Hooks.namespaces.stream(), options.hookNamespaces.stream())
-        .anyMatch(ns -> hook.startsWith(ns + "."));
-  }
-
-  private static boolean isBuiltinProduction(Production prod) {
-    return prod.klabel().nonEmpty() && ConstructorChecks.isBuiltinLabel(prod.klabel().get());
-  }
-
   public String convertSpecificationModule(
       Module definition, Module spec, SentenceType defaultSentenceType, StringBuilder sb) {
     SentenceType sentenceType = getSentenceType(spec.att()).orElse(defaultSentenceType);
@@ -1625,13 +1615,30 @@ private void convertParams(Option<KLabel> maybeKLabel, boolean hasR, StringBuild
   }
 
   private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {
-    Att att = addKoreAttributes(prod, functionRules, java.util.Collections.emptySet());
+    Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet());
     return att.contains(Att.CONSTRUCTOR());
   }
 
-  private boolean isFunctional(Production prod, SetMultimap<KLabel, Rule> functionRules) {
-    Att att = addKoreAttributes(prod, functionRules, java.util.Collections.emptySet());
-    return att.contains(Att.FUNCTIONAL());
+  private static boolean isFunctional(Production prod) {
+    return !isFunction(prod) || prod.att().contains(Att.TOTAL());
+  }
+
+  private static boolean isFunction(Production prod) {
+    return prod.att().contains(Att.FUNCTION());
+  }
+
+  private boolean isHook(Production prod) {
+    return prod.att().contains(Att.HOOK()) && isRealHook(prod.att());
+  }
+
+  private boolean isRealHook(Att att) {
+    String hook = att.get(Att.HOOK());
+    return Stream.concat(Hooks.namespaces.stream(), options.hookNamespaces.stream())
+        .anyMatch(ns -> hook.startsWith(ns + "."));
+  }
+
+  private static boolean isBuiltinProduction(Production prod) {
+    return prod.klabel().nonEmpty() && ConstructorChecks.isBuiltinLabel(prod.klabel().get());
   }
 
   private boolean isGeneratedInKeysOp(Production prod) {
@@ -1641,9 +1648,16 @@ private boolean isGeneratedInKeysOp(Production prod) {
     return (!prod.klabel().isEmpty());
   }
 
-  private Att addKoreAttributes(
+  private Att koreAttributes(
+      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
+    Att att = prod.att().remove(Att.CONSTRUCTOR()).remove(Att.HOOK()).remove(Att.FORMAT());
+    att = att.addAll(semanticAttributes(prod, functionRules, overloads));
+    att = att.addAll(syntaxAttributes(prod));
+    return att;
+  }
+
+  private Att semanticAttributes(
       Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
-    boolean isFunctional = !isFunction(prod) || prod.att().contains(Att.TOTAL());
     boolean isConstructor = !isFunction(prod);
     isConstructor &= !prod.att().contains(Att.ASSOC());
     isConstructor &= !prod.att().contains(Att.COMM());
@@ -1667,14 +1681,14 @@ private Att addKoreAttributes(
     isConstructor &= !isMacro;
     isConstructor &= !isAnywhere;
 
-    Att att = prod.att().remove(Att.CONSTRUCTOR());
-    if (att.contains(Att.HOOK()) && !isRealHook(att)) {
-      att = att.remove(Att.HOOK());
+    Att att = Att.empty();
+    if (isHook(prod)) {
+      att = att.add(Att.HOOK(), prod.att().get(att.HOOK()));
     }
     if (isConstructor) {
       att = att.add(Att.CONSTRUCTOR());
     }
-    if (isFunctional) {
+    if (isFunctional(prod)) {
       att = att.add(Att.FUNCTIONAL());
     }
     if (isAnywhere) {
@@ -1686,10 +1700,13 @@ private Att addKoreAttributes(
     if (isMacro) {
       att = att.add(Att.MACRO());
     }
+    return att;
+  }
+
+  private Att syntaxAttributes(Production prod) {
     // update format attribute with structure expected by backend
-    String format = att.getOptional(Att.FORMAT()).orElse(prod.defaultFormat());
+    String format = prod.att().getOptional(Att.FORMAT()).orElse(prod.defaultFormat());
     int nt = 1;
-    boolean hasFormat = true;
 
     for (int i = 0; i < prod.items().size(); i++) {
       if (prod.items().apply(i) instanceof NonTerminal) {
@@ -1707,48 +1724,45 @@ private Att addKoreAttributes(
                         .replace("%", "%%")
                     + "%r");
       } else {
-        hasFormat = false;
+        return Att.empty();
       }
     }
-    if (hasFormat) {
-      att = att.add(Att.FORMAT(), format);
-      if (att.contains(Att.COLOR())) {
-        boolean escape = false;
-        StringBuilder colors = new StringBuilder();
-        String conn = "";
-        for (int i = 0; i < format.length(); i++) {
-          if (escape && format.charAt(i) == 'c') {
-            colors.append(conn).append(att.get(Att.COLOR()));
-            conn = ",";
-          }
-          escape = format.charAt(i) == '%';
-        }
-        att = att.add(Att.COLORS(), colors.toString());
-      }
-      StringBuilder sb = new StringBuilder();
-      for (ProductionItem pi : iterable(prod.items())) {
-        if (pi instanceof NonTerminal) {
-          sb.append('0');
-        } else {
-          sb.append('1');
+
+    Att att = Att.empty();
+    att = att.add(Att.FORMAT(), format);
+    if (prod.att().contains(Att.COLOR())) {
+      String color = prod.att().get(Att.COLOR());
+      boolean escape = false;
+      StringBuilder colors = new StringBuilder();
+      String conn = "";
+      for (int i = 0; i < format.length(); i++) {
+        if (escape && format.charAt(i) == 'c') {
+          colors.append(conn).append(color);
+          conn = ",";
         }
+        escape = format.charAt(i) == '%';
       }
-      att = att.add(Att.TERMINALS(), sb.toString());
-      if (prod.klabel().isDefined()) {
-        att = att.add(Att.PRIORITIES(), KList.class, getPriorities(prod.klabel().get()));
-        att =
-            att.add(
-                Att.LEFT_INTERNAL(),
-                KList.class,
-                getAssoc(module.leftAssoc(), prod.klabel().get()));
-        att =
-            att.add(
-                Att.RIGHT_INTERNAL(),
-                KList.class,
-                getAssoc(module.rightAssoc(), prod.klabel().get()));
+      att = att.add(Att.COLORS(), colors.toString());
+    }
+    StringBuilder sb = new StringBuilder();
+    for (ProductionItem pi : iterable(prod.items())) {
+      if (pi instanceof NonTerminal) {
+        sb.append('0');
+      } else {
+        sb.append('1');
       }
-    } else {
-      att = att.remove(Att.FORMAT());
+    }
+    att = att.add(Att.TERMINALS(), sb.toString());
+    if (prod.klabel().isDefined()) {
+      att = att.add(Att.PRIORITIES(), KList.class, getPriorities(prod.klabel().get()));
+      att =
+          att.add(
+              Att.LEFT_INTERNAL(), KList.class, getAssoc(module.leftAssoc(), prod.klabel().get()));
+      att =
+          att.add(
+              Att.RIGHT_INTERNAL(),
+              KList.class,
+              getAssoc(module.rightAssoc(), prod.klabel().get()));
     }
     return att;
   }
@@ -1781,10 +1795,6 @@ private KList getAssoc(scala.collection.Set<Tuple2<Tag, Tag>> assoc, KLabel klab
             .collect(Collectors.toList()));
   }
 
-  private boolean isFunction(Production prod) {
-    return prod.att().contains(Att.FUNCTION());
-  }
-
   // Assume that there is no quantifiers
   private Set<KVariable> collectLHSFreeVariables(K requires, K left) {
     Set<KVariable> res = new HashSet<>();