diff --git a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java b/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java
deleted file mode 100644
index c7e8f735642..00000000000
--- a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java
+++ /dev/null
@@ -1,165 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework.compile;
-
-import static org.kframework.definition.Constructors.*;
-import static org.kframework.kore.KORE.*;
-
-import java.util.HashSet;
-import java.util.Optional;
-import java.util.Set;
-import org.kframework.builtin.BooleanUtils;
-import org.kframework.builtin.Sorts;
-import org.kframework.definition.Context;
-import org.kframework.definition.Rule;
-import org.kframework.definition.Sentence;
-import org.kframework.kore.*;
-
-/**
- * Transforms patterns in the LHS of rules which have tokens of sort Int or Float into side
- * conditions generating equality over a reconstructed value. Thus,
- *
- * <p>rule 5 => .K
- *
- * <p>becomes
- *
- * <p>rule I:Int => .K when I ==K 5
- */
-public class DeconstructIntegerAndFloatLiterals {
-
-  private final Set<KApply> state = new HashSet<>();
-  private final Set<KVariable> vars = new HashSet<>();
-
-  void reset() {
-    state.clear();
-    vars.clear();
-  }
-
-  void gatherVars(K term) {
-    new VisitK() {
-      @Override
-      public void apply(KVariable v) {
-        vars.add(v);
-        super.apply(v);
-      }
-    }.apply(term);
-  }
-
-  public Sentence convert(Sentence s) {
-    if (ExpandMacros.isMacro(s)) {
-      return s;
-    }
-    if (s instanceof Rule) {
-      return convert((Rule) s);
-    } else if (s instanceof Context) {
-      return convert((Context) s);
-    } else {
-      return s;
-    }
-  }
-
-  private Rule convert(Rule rule) {
-    reset();
-    gatherVars(rule.body());
-    gatherVars(rule.requires());
-    gatherVars(rule.ensures());
-    K body = convert(rule.body());
-    K requires = convertLookups(rule.requires());
-    return Rule(body, addSideCondition(requires), rule.ensures(), rule.att());
-  }
-
-  private K convertLookups(K requires) {
-    return new Transformer(false).apply(requires);
-  }
-
-  private Context convert(Context context) {
-    reset();
-    gatherVars(context.body());
-    gatherVars(context.requires());
-    K body = convert(context.body());
-    return Context(body, addSideCondition(context.requires()), context.att());
-  }
-
-  private int counter = 0;
-
-  KVariable newDotVariable(Sort sort) {
-    KVariable newLabel;
-    do {
-      newLabel = KVariable("_Gen" + (counter++), Att().add(Sort.class, sort));
-    } while (vars.contains(newLabel));
-    vars.add(newLabel);
-    return newLabel;
-  }
-
-  K addSideCondition(K requires) {
-    Optional<KApply> sideCondition = state.stream().reduce(BooleanUtils::and);
-    if (sideCondition.isEmpty()) {
-      return requires;
-    } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) {
-      return sideCondition.get();
-    } else {
-      return BooleanUtils.and(requires, sideCondition.get());
-    }
-  }
-
-  private K convert(K term) {
-    return new Transformer(true).apply(term);
-  }
-
-  private class Transformer extends TransformK {
-
-    @Override
-    public K apply(KToken k) {
-      if (lhs) {
-        if (k.sort().equals(Sorts.Int()) || k.sort().equals(Sorts.Float())) {
-          KVariable var = newDotVariable(k.sort());
-          state.add(KApply(KLabel("_==" + k.sort().name() + "_"), var, k));
-          return var;
-        }
-      }
-      return super.apply(k);
-    }
-
-    private boolean lhs;
-
-    public Transformer(boolean lhs) {
-      this.lhs = lhs;
-    }
-
-    public boolean isLookupKLabel(KLabel k) {
-      return k.name().equals("#match")
-          || k.name().equals("#mapChoice")
-          || k.name().equals("#filterMapChoice")
-          || k.name().equals("#setChoice");
-    }
-
-    @Override
-    public K apply(KApply k) {
-      if (isLookupKLabel(k.klabel())) {
-        assert k.klist().size() == 2;
-        K r = apply(k.klist().items().get(1));
-        lhs = true;
-        K l = apply(k.klist().items().get(0));
-        lhs = false;
-        if (l != k.klist().items().get(0) || r != k.klist().items().get(1)) {
-          return KApply(k.klabel(), l, r);
-        } else {
-          return k;
-        }
-      }
-      return super.apply(k);
-    }
-
-    @Override
-    public K apply(KRewrite k) {
-      K l = apply(k.left());
-      lhs = false;
-      K r = apply(k.right());
-      lhs = true;
-      if (l != k.left() || r != k.right()) {
-        return KRewrite(l, r, k.att());
-      } else {
-        return k;
-      }
-    }
-  }
-}
diff --git a/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java b/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java
deleted file mode 100644
index 6e54a69593e..00000000000
--- a/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java
+++ /dev/null
@@ -1,85 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework.compile;
-
-import static org.kframework.definition.Constructors.*;
-import static org.kframework.kore.KORE.*;
-
-import java.util.ArrayList;
-import java.util.List;
-import org.kframework.builtin.KLabels;
-import org.kframework.builtin.Sorts;
-import org.kframework.definition.Context;
-import org.kframework.definition.Rule;
-import org.kframework.definition.Sentence;
-import org.kframework.kore.*;
-
-/**
- * Raises all rules into a form with a KSequence in every position that expects a term of sort K.
- */
-public class LiftToKSequence {
-
-  public Sentence lift(Sentence s) {
-    if (s instanceof Rule) {
-      return lift((Rule) s);
-    } else if (s instanceof Context) {
-      return lift((Context) s);
-    } else {
-      return s;
-    }
-  }
-
-  private Rule lift(Rule rule) {
-    return Rule(lift(rule.body()), lift(rule.requires()), lift(rule.ensures()), rule.att());
-  }
-
-  private Context lift(Context context) {
-    return Context(lift(context.body()), lift(context.requires()), context.att());
-  }
-
-  public K lift(K term) {
-    K result =
-        new TransformK() {
-          @Override
-          public K apply(KApply k) {
-            List<K> children = new ArrayList<>();
-            for (K child : k.klist().items()) {
-              K res = apply(child);
-              if (res instanceof KSequence || k.klabel().equals(KLabels.ML_OR)) {
-                children.add(res);
-              } else {
-                children.add(KSequence(res));
-              }
-            }
-            return KApply(k.klabel(), KList(children), k.att());
-          }
-
-          @Override
-          public K apply(KAs k) {
-            K res = apply(k.pattern());
-            KVariable var = (KVariable) k.alias();
-            if (!(res instanceof KSequence)
-                && var.att().getOptional(Sort.class).orElse(Sorts.K()).equals(Sorts.K())) {
-              res = KSequence(res);
-            }
-            return KAs(res, k.alias(), k.att());
-          }
-        }.apply(term);
-    if (result instanceof KSequence) {
-      return result;
-    } else {
-      return KSequence(result);
-    }
-  }
-
-  public K lower(K term) {
-    return new TransformK() {
-      @Override
-      public K apply(KSequence k) {
-        if (k.items().size() == 1) {
-          return super.apply(k.items().get(0));
-        }
-        return super.apply(k);
-      }
-    }.apply(term);
-  }
-}
diff --git a/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java b/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java
deleted file mode 100644
index ac4b2bf3e8a..00000000000
--- a/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java
+++ /dev/null
@@ -1,42 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework.main;
-
-import com.google.inject.Binding;
-import com.google.inject.Key;
-import com.google.inject.Module;
-import com.google.inject.PrivateModule;
-import com.google.inject.spi.DefaultElementVisitor;
-import com.google.inject.spi.Element;
-import com.google.inject.spi.Elements;
-import java.lang.annotation.Annotation;
-import java.util.List;
-import java.util.function.Function;
-
-public abstract class AnnotatedByDefinitionModule extends PrivateModule {
-
-  public void exposeBindings(List<Module> modules, Class cls, Function<Class, Annotation> func) {
-    for (Element element : Elements.getElements(modules)) {
-      element.acceptVisitor(
-          new DefaultElementVisitor<Void>() {
-            @Override
-            public <T> Void visit(Binding<T> binding) {
-              Key<T> key = binding.getKey();
-              if (key.getAnnotation() == null && key.getAnnotationType() == null) {
-                bind(key.getTypeLiteral()).annotatedWith(cls).to(key.getTypeLiteral());
-                expose(key.getTypeLiteral()).annotatedWith(cls);
-              } else if (key.getAnnotationType() != null
-                  && !key.getAnnotationType()
-                      .getPackage()
-                      .equals(Package.getPackage("com.google.inject.multibindings"))) {
-                bind(key.getTypeLiteral())
-                    .annotatedWith(func.apply(key.getAnnotationType()))
-                    .to(key);
-                expose(key.getTypeLiteral()).annotatedWith(func.apply(key.getAnnotationType()));
-              }
-              return null;
-            }
-          });
-    }
-    modules.forEach(AnnotatedByDefinitionModule.this::install);
-  }
-}
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Builtins.java b/kernel/src/main/java/org/kframework/utils/inject/Builtins.java
deleted file mode 100644
index 7cd73a2ee7c..00000000000
--- a/kernel/src/main/java/org/kframework/utils/inject/Builtins.java
+++ /dev/null
@@ -1,16 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework.utils.inject;
-
-import static java.lang.annotation.ElementType.FIELD;
-import static java.lang.annotation.ElementType.METHOD;
-import static java.lang.annotation.ElementType.PARAMETER;
-import static java.lang.annotation.RetentionPolicy.RUNTIME;
-
-import com.google.inject.BindingAnnotation;
-import java.lang.annotation.Retention;
-import java.lang.annotation.Target;
-
-@BindingAnnotation
-@Target({FIELD, PARAMETER, METHOD})
-@Retention(RUNTIME)
-public @interface Builtins {}
diff --git a/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java b/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java
deleted file mode 100644
index ee60c792ed8..00000000000
--- a/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java
+++ /dev/null
@@ -1,24 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework.utils.options;
-
-import com.beust.jcommander.ParameterException;
-import com.beust.jcommander.converters.BaseConverter;
-
-public class OnOffConverter extends BaseConverter<Boolean> {
-
-  public OnOffConverter(String optionName) {
-    super(optionName);
-  }
-
-  @Override
-  public Boolean convert(String arg0) {
-    if (arg0.equals("on")) {
-      return true;
-    } else if (arg0.equals("off")) {
-      return false;
-    } else {
-      throw new ParameterException(
-          "\"" + getOptionName() + "\": must be either \"on\" or \"off\".");
-    }
-  }
-}
diff --git a/kore/src/main/java/org/kframework/API.java b/kore/src/main/java/org/kframework/API.java
deleted file mode 100644
index aa1aecdffe2..00000000000
--- a/kore/src/main/java/org/kframework/API.java
+++ /dev/null
@@ -1,12 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework;
-
-import java.lang.annotation.ElementType;
-import java.lang.annotation.Target;
-
-/**
- * Marker for classes we consider as part fo the K API. It is particularly important for these
- * classes to be well-documented.
- */
-@Target(ElementType.TYPE)
-public @interface API {}
diff --git a/kore/src/main/java/org/kframework/Warning.java b/kore/src/main/java/org/kframework/Warning.java
deleted file mode 100644
index 16c858e45ea..00000000000
--- a/kore/src/main/java/org/kframework/Warning.java
+++ /dev/null
@@ -1,5 +0,0 @@
-// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-package org.kframework;
-
-@API
-public interface Warning {}