diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
index 1466abd5b64..d43f55fc1fb 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
@@ -356,7 +356,7 @@ private RewriterResult executeKoreCommands(Module rules, String[] koreCommand,
             @Override
             public RewriterResult prove(Module rules, Rule boundaryPattern, Boolean reuseDef) {
                 Module kompiledModule = KoreBackend.getKompiledModule(module);
-                ModuleToKORE converter = new ModuleToKORE(kompiledModule, def.topCellInitializer, kompileOptions);
+                ModuleToKORE converter = new ModuleToKORE(kompiledModule, def.topCellInitializer, kompileOptions, kem);
                 String defPath = reuseDef ? files.resolveKompiled("definition.kore").getAbsolutePath() : saveKoreDefinitionToTemp(converter);
                 String specPath = saveKoreSpecToTemp(converter, rules);
                 File koreOutputFile = files.resolveTemp("result.kore");
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 1ace66863cd..49ae5ee0b21 100644
--- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
+++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -45,6 +45,8 @@
 import org.kframework.unparser.Formatter;
 import org.kframework.utils.StringUtil;
 import org.kframework.utils.errorsystem.KEMException;
+import org.kframework.utils.errorsystem.KException;
+import org.kframework.utils.errorsystem.KExceptionManager;
 import scala.Option;
 import scala.Tuple2;
 import scala.collection.JavaConverters;
@@ -107,7 +109,14 @@ public enum SentenceType {
     private final Set<String> mlBinders = new HashSet<>();
     private final KompileOptions options;
 
+    private final KExceptionManager kem;
+
     public ModuleToKORE(Module module, KLabel topCellInitializer, KompileOptions options) {
+        this(module, topCellInitializer, options, null);
+    }
+
+    public ModuleToKORE(Module module, KLabel topCellInitializer, KompileOptions options, KExceptionManager kem) {
+        this.kem = kem;
         this.module = module;
         this.addSortInjections = new AddSortInjections(module);
         this.topCellInitializer = topCellInitializer;
@@ -941,7 +950,13 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
                 .stream().collect(Collectors.toMap(KVariable::name, Function.identity()));
         if (ruleInfo.isEquation) {
             assertNoExistentials(rule, existentials);
-            sb.append("  axiom{R");
+            if (rule instanceof Claim) {
+                sb.append("  claim{R");
+                if (kem != null) // TODO: remove once https://github.com/runtimeverification/haskell-backend/issues/3010 is implemented
+                    kem.registerCompilerWarning(KException.ExceptionType.FUTURE_ERROR, "Functional claims not yet supported. https://github.com/runtimeverification/haskell-backend/issues/3010", rule);
+            } else {
+                sb.append("  axiom{R");
+            }
             Option<Sort> sortParamsWrapper = rule.att().getOption("sortParams", Sort.class);
             Option<Set<String>> sortParams = sortParamsWrapper.map(s -> stream(s.params()).map(sort -> sort.name()).collect(Collectors.toSet()));
             if (sortParams.nonEmpty()) {
@@ -1054,7 +1069,7 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
                 sb.append(")))\n  ");
                 convert(consideredAttributes, rule.att(), sb, freeVarsMap, rule);
                 sb.append("\n\n");
-            } else if (rule.att().contains(Att.SIMPLIFICATION())) {
+            } else if (rule.att().contains(Att.SIMPLIFICATION()) || rule instanceof Claim) {
                 sb.append("\\implies{R} (\n    ");
                 convertSideCondition(requires, sb);
                 sb.append(",\n    \\equals{");