diff --git a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
index fc01ab57035..2121936d6c9 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
@@ -1,5 +1,5 @@
 // Copyright (c) K Team. All Rights Reserved.
-package org.kframework.parser.kore  
+package org.kframework.parser.kore
 
 import com.davekoelle.AlphanumComparator
 import org.kframework.utils.errorsystem.KEMException
@@ -109,7 +109,7 @@ trait AxiomDeclaration extends Declaration {
   def att: Attributes
 }
 
-trait ClaimDeclaration extends  AxiomDeclaration {}
+trait ClaimDeclaration extends AxiomDeclaration {}
 
 object AxiomDeclaration {
   def unapply(arg: AxiomDeclaration): Option[(Seq[SortVariable], Pattern, Attributes)]
@@ -129,69 +129,67 @@ trait Pattern extends Comparable[Pattern] {
 }
 
 object AlphanumOrdering extends Ordering[String] {
-  def compare(a:String, b:String): Int = new AlphanumComparator().compare(a, b)
+  def compare(a: String, b: String): Int = new AlphanumComparator().compare(a, b)
 }
- 
+
 object Pattern {
-  implicit val ord = new Ordering[Pattern] {
-    def compare(a: Pattern, b: Pattern): Int = {
-      (a, b) match {
-        case (c:Variable, d:Variable) => Ordering[Variable].compare(c, d)
-        case (c:Application, d:Application) => Ordering[Application].compare(c, d)
-        case (c:Top, d:Top) => Ordering[Top].compare(c, d)
-        case (c:Bottom, d:Bottom) => Ordering[Bottom].compare(c, d)
-        case (c:And, d:And) => Ordering[And].compare(c, d)
-        case (c:Or, d:Or) => Ordering[Or].compare(c, d)
-        case (c:Not, d:Not) => Ordering[Not].compare(c, d)
-        case (c:Implies, d:Implies) => Ordering[Implies].compare(c, d)
-        case (c:Iff, d:Iff) => Ordering[Iff].compare(c, d)
-        case (c:Exists, d:Exists) => Ordering[Exists].compare(c, d)
-        case (c:Forall, d:Forall) => Ordering[Forall].compare(c, d)
-        case (c:Ceil, d:Ceil) => Ordering[Ceil].compare(c, d)
-        case (c:Floor, d:Floor) => Ordering[Floor].compare(c, d)
-        case (c:Rewrites, d:Rewrites) => Ordering[Rewrites].compare(c, d)
-        case (c:Equals, d:Equals) => Ordering[Equals].compare(c, d)
-        case (c:Mem, d:Mem) => Ordering[Mem].compare(c, d)
-        case (c:DomainValue, d:DomainValue) => Ordering[DomainValue].compare(c, d)
-        case (c:StringLiteral, d:StringLiteral) => Ordering[StringLiteral].compare(c, d)
-        case (_:Variable, _) => -1
-        case (_, _:Variable) => 1
-        case (_:Application, _) => -1
-        case (_, _:Application) => 1
-        case (_:Top, _) => -1
-        case (_, _:Top) => 1
-        case (_:Bottom, _) => -1
-        case (_, _:Bottom) => 1
-        case (_:And, _) => -1
-        case (_, _:And) => 1
-        case (_:Or, _) => -1
-        case (_, _:Or) => 1
-        case (_:Not, _) => -1
-        case (_, _:Not) => 1
-        case (_:Implies, _) => -1
-        case (_, _:Implies) => 1
-        case (_:Iff, _) => -1
-        case (_, _:Iff) => 1
-        case (_:Exists, _) => -1
-        case (_, _:Exists) => 1
-        case (_:Forall, _) => -1
-        case (_, _:Forall) => 1
-        case (_:Ceil, _) => -1
-        case (_, _:Ceil) => 1
-        case (_:Floor, _) => -1
-        case (_, _:Floor) => 1
-        case (_:Rewrites, _) => -1
-        case (_, _:Rewrites) => 1
-        case (_:Equals, _) => -1
-        case (_, _:Equals) => 1
-        case (_:Mem, _) => -1
-        case (_, _:Mem) => 1
-        case (_:DomainValue, _) => -1
-        case (_, _:DomainValue) => 1
-        case (_:StringLiteral, _) => -1
-        case (_, _:StringLiteral) => 1
-        case (_, _) => throw KEMException.internalError("Cannot order these patterns:\n" + a.toString() + "\n" + b.toString())
-      }
+  implicit val ord: Ordering[Pattern] = (a: Pattern, b: Pattern) => {
+    (a, b) match {
+      case (c: Variable, d: Variable) => Ordering[Variable].compare(c, d)
+      case (c: Application, d: Application) => Ordering[Application].compare(c, d)
+      case (c: Top, d: Top) => Ordering[Top].compare(c, d)
+      case (c: Bottom, d: Bottom) => Ordering[Bottom].compare(c, d)
+      case (c: And, d: And) => Ordering[And].compare(c, d)
+      case (c: Or, d: Or) => Ordering[Or].compare(c, d)
+      case (c: Not, d: Not) => Ordering[Not].compare(c, d)
+      case (c: Implies, d: Implies) => Ordering[Implies].compare(c, d)
+      case (c: Iff, d: Iff) => Ordering[Iff].compare(c, d)
+      case (c: Exists, d: Exists) => Ordering[Exists].compare(c, d)
+      case (c: Forall, d: Forall) => Ordering[Forall].compare(c, d)
+      case (c: Ceil, d: Ceil) => Ordering[Ceil].compare(c, d)
+      case (c: Floor, d: Floor) => Ordering[Floor].compare(c, d)
+      case (c: Rewrites, d: Rewrites) => Ordering[Rewrites].compare(c, d)
+      case (c: Equals, d: Equals) => Ordering[Equals].compare(c, d)
+      case (c: Mem, d: Mem) => Ordering[Mem].compare(c, d)
+      case (c: DomainValue, d: DomainValue) => Ordering[DomainValue].compare(c, d)
+      case (c: StringLiteral, d: StringLiteral) => Ordering[StringLiteral].compare(c, d)
+      case (_: Variable, _) => -1
+      case (_, _: Variable) => 1
+      case (_: Application, _) => -1
+      case (_, _: Application) => 1
+      case (_: Top, _) => -1
+      case (_, _: Top) => 1
+      case (_: Bottom, _) => -1
+      case (_, _: Bottom) => 1
+      case (_: And, _) => -1
+      case (_, _: And) => 1
+      case (_: Or, _) => -1
+      case (_, _: Or) => 1
+      case (_: Not, _) => -1
+      case (_, _: Not) => 1
+      case (_: Implies, _) => -1
+      case (_, _: Implies) => 1
+      case (_: Iff, _) => -1
+      case (_, _: Iff) => 1
+      case (_: Exists, _) => -1
+      case (_, _: Exists) => 1
+      case (_: Forall, _) => -1
+      case (_, _: Forall) => 1
+      case (_: Ceil, _) => -1
+      case (_, _: Ceil) => 1
+      case (_: Floor, _) => -1
+      case (_, _: Floor) => 1
+      case (_: Rewrites, _) => -1
+      case (_, _: Rewrites) => 1
+      case (_: Equals, _) => -1
+      case (_, _: Equals) => 1
+      case (_: Mem, _) => -1
+      case (_, _: Mem) => 1
+      case (_: DomainValue, _) => -1
+      case (_, _: DomainValue) => 1
+      case (_: StringLiteral, _) => -1
+      case (_, _: StringLiteral) => 1
+      case (_, _) => throw KEMException.internalError("Cannot order these patterns:\n" + a.toString + "\n" + b.toString)
     }
   }
 }
@@ -203,8 +201,8 @@ trait Variable extends Pattern {
 }
 
 object Variable {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Variable): Option[(String, Sort)] = Some(arg.name, arg.sort)
+
   implicit val ord: Ordering[Variable] = Ordering.by(unapply)
 }
 
@@ -217,8 +215,11 @@ trait Application extends Pattern {
 }
 
 object Application {
+
   import scala.math.Ordering.Implicits._
+
   def unapply(arg: Application): Option[(SymbolOrAlias, Seq[Pattern])] = Some(arg.head, arg.args)
+
   implicit val ord: Ordering[Application] = Ordering.by(unapply)
 }
 
@@ -227,8 +228,8 @@ trait Top extends Pattern {
 }
 
 object Top {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Top): Option[Sort] = Some(arg.s)
+
   implicit val ord: Ordering[Top] = Ordering.by(unapply)
 }
 
@@ -237,8 +238,8 @@ trait Bottom extends Pattern {
 }
 
 object Bottom {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Bottom): Option[Sort] = Some(arg.s)
+
   implicit val ord: Ordering[Bottom] = Ordering.by(unapply)
 }
 
@@ -249,8 +250,11 @@ trait And extends Pattern {
 }
 
 object And {
+
   import scala.math.Ordering.Implicits._
+
   def unapply(arg: And): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
+
   implicit val ord: Ordering[And] = Ordering.by(unapply)
 }
 
@@ -261,8 +265,11 @@ trait Or extends Pattern {
 }
 
 object Or {
+
   import scala.math.Ordering.Implicits._
+
   def unapply(arg: Or): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
+
   implicit val ord: Ordering[Or] = Ordering.by(unapply)
 }
 
@@ -273,8 +280,8 @@ trait Not extends Pattern {
 }
 
 object Not {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Not): Option[(Sort, Pattern)] = Some(arg.s, arg._1)
+
   implicit val ord: Ordering[Not] = Ordering.by(unapply)
 }
 
@@ -287,8 +294,8 @@ trait Implies extends Pattern {
 }
 
 object Implies {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Implies): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
+
   implicit val ord: Ordering[Implies] = Ordering.by(unapply)
 }
 
@@ -301,8 +308,8 @@ trait Iff extends Pattern {
 }
 
 object Iff {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Iff): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
+
   implicit val ord: Ordering[Iff] = Ordering.by(unapply)
 }
 
@@ -315,8 +322,8 @@ trait Exists extends Pattern {
 }
 
 object Exists {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Exists): Option[(Sort, Variable, Pattern)] = Some(arg.s, arg.v, arg.p)
+
   implicit val ord: Ordering[Exists] = Ordering.by(unapply)
 }
 
@@ -329,8 +336,8 @@ trait Forall extends Pattern {
 }
 
 object Forall {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Forall): Option[(Sort, Variable, Pattern)] = Some(arg.s, arg.v, arg.p)
+
   implicit val ord: Ordering[Forall] = Ordering.by(unapply)
 }
 
@@ -343,8 +350,8 @@ trait Ceil extends Pattern {
 }
 
 object Ceil {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Ceil): Option[(Sort, Sort, Pattern)] = Some(arg.s, arg.rs, arg.p)
+
   implicit val ord: Ordering[Ceil] = Ordering.by(unapply)
 }
 
@@ -357,8 +364,8 @@ trait Floor extends Pattern {
 }
 
 object Floor {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Floor): Option[(Sort, Sort, Pattern)] = Some(arg.s, arg.rs, arg.p)
+
   implicit val ord: Ordering[Floor] = Ordering.by(unapply)
 }
 // trait Next extends Pattern {
@@ -373,33 +380,36 @@ object Floor {
 
 trait GeneralizedRewrite {
   def sort: Sort
+
   def getLeftHandSide: Seq[Pattern]
+
   def getRightHandSide: Pattern
 }
 
 /**
-  * \rewrites(P, Q) is defined as a predicate pattern floor(P implies Q)
-  * Therefore a rewrites-to pattern is parametric on two sorts.
-  * One is the sort of patterns P and Q;
-  * The other is the sort of the context.
-  */
+ * \rewrites(P, Q) is defined as a predicate pattern floor(P implies Q)
+ * Therefore a rewrites-to pattern is parametric on two sorts.
+ * One is the sort of patterns P and Q;
+ * The other is the sort of the context.
+ */
 trait Rewrites extends Pattern with GeneralizedRewrite {
   def s: Sort // the sort of the two patterns P and Q
 
-  def sort = s
+  def sort: Sort = s
 
   def _1: Pattern
 
   def _2: Pattern
 
-  def getLeftHandSide = Seq(_1)
-  def getRightHandSide = _2
+  def getLeftHandSide: Seq[Pattern] = Seq(_1)
+
+  def getRightHandSide: Pattern = _2
 }
 
 object Rewrites {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Rewrites): Option[(Sort, Pattern, Pattern)] =
     Some(arg.s, arg._1, arg._2)
+
   implicit val ord: Ordering[Rewrites] = Ordering.by(unapply)
 }
 
@@ -408,28 +418,28 @@ trait Equals extends Pattern with GeneralizedRewrite {
 
   def rs: Sort // the sort of the context where the equality pattern is being placed
 
-  def sort = rs
+  def sort: Sort = rs
 
   def _1: Pattern
 
   def _2: Pattern
 
-  def getLeftHandSide = _1 match {
+  def getLeftHandSide: Seq[Pattern] = _1 match {
     case Application(_, ps) => ps
   }
 
-  def getRightHandSide = _2
+  def getRightHandSide: Pattern = _2
 }
 
 object Equals {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Equals): Option[(Sort, Sort, Pattern, Pattern)] = Some(arg.s, arg.rs, arg._1, arg._2)
+
   implicit val ord: Ordering[Equals] = Ordering.by(unapply)
 }
 
 /**
-  * Membership, denoted as \in(P, Q) === \ceil(P and Q)
-  */
+ * Membership, denoted as \in(P, Q) === \ceil(P and Q)
+ */
 trait Mem extends Pattern {
   def s: Sort // the sort of X and P
 
@@ -441,14 +451,14 @@ trait Mem extends Pattern {
 }
 
 object Mem {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: Mem): Option[(Sort, Sort, Pattern, Pattern)] = Some(arg.s, arg.rs, arg.p, arg.q)
+
   implicit val ord: Ordering[Mem] = Ordering.by(unapply)
 }
 
 /**
-  * Any domain-specific value represented as a string.
-  */
+ * Any domain-specific value represented as a string.
+ */
 trait DomainValue extends Pattern {
   def s: Sort // the sort of X and P
 
@@ -456,15 +466,16 @@ trait DomainValue extends Pattern {
 }
 
 object DomainValue {
-  import scala.math.Ordering.Implicits._
   implicit val strOrd: Ordering[String] = AlphanumOrdering
+
   def unapply(arg: DomainValue): Option[(Sort, String)] = Some(arg.s, arg.str)
+
   implicit val ord: Ordering[DomainValue] = Ordering.by(unapply)
 }
 
 /**
-  * \subset(P,Q) is a predicate pattern that checks whether P is a subset of Q.
-  */
+ * \subset(P,Q) is a predicate pattern that checks whether P is a subset of Q.
+ */
 // trait Subset extends Pattern {
 //   def s: Sort // the sort of P and Q
 //
@@ -486,8 +497,8 @@ trait StringLiteral extends Pattern {
 }
 
 object StringLiteral {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: StringLiteral): Option[String] = Some(arg.str)
+
   implicit val ord: Ordering[StringLiteral] = Ordering.by(unapply)
 }
 
@@ -507,25 +518,23 @@ object StringLiteral {
 
 
 /** A sort can be either a sort variable or of the form C{s1,...,sn}
-  * where C is called the sort constructor and s1,...,sn are sort parameters.
-  * We call sorts that are of the form C{s1,...,sn} compound sorts because
-  * I don't know a better name.
-  */
+ * where C is called the sort constructor and s1,...,sn are sort parameters.
+ * We call sorts that are of the form C{s1,...,sn} compound sorts because
+ * I don't know a better name.
+ */
 
 trait Sort
 
 object Sort {
-  implicit val ord = new Ordering[Sort] {
-    def compare(a: Sort, b: Sort): Int = {
-      (a, b) match {
-        case (c:SortVariable, d:SortVariable) => Ordering[SortVariable].compare(c, d)
-        case (c:CompoundSort, d:CompoundSort) => Ordering[CompoundSort].compare(c, d)
-        case (_:SortVariable, _) => -1
-        case (_, _:SortVariable) => 1
-        case (_:CompoundSort, _) => -1
-        case (_, _:CompoundSort) => 1
-        case (_, _) => throw KEMException.internalError("Cannot order these sorts:\n" + a.toString() + "\n" + b.toString())
-      }
+  implicit val ord: Ordering[Sort] = (a: Sort, b: Sort) => {
+    (a, b) match {
+      case (c: SortVariable, d: SortVariable) => Ordering[SortVariable].compare(c, d)
+      case (c: CompoundSort, d: CompoundSort) => Ordering[CompoundSort].compare(c, d)
+      case (_: SortVariable, _) => -1
+      case (_, _: SortVariable) => 1
+      case (_: CompoundSort, _) => -1
+      case (_, _: CompoundSort) => 1
+      case (_, _) => throw KEMException.internalError("Cannot order these sorts:\n" + a.toString + "\n" + b.toString)
     }
   }
 }
@@ -535,30 +544,34 @@ trait SortVariable extends Sort {
 }
 
 object SortVariable {
-  import scala.math.Ordering.Implicits._
   def unapply(arg: SortVariable): Option[String] = Some(arg.name)
+
   implicit val ord: Ordering[SortVariable] = Ordering.by(unapply)
 }
 
 /** A compound sort is of the form C{s1,...,sn}
-  * For example:
-  * Nat{} List{Nat{}} List{S} Map{S,List{S}} Map{Map{Nat{},Nat{}},Nat{}}
-  */
+ * For example:
+ * Nat{} List{Nat{}} List{S} Map{S,List{S}} Map{Map{Nat{},Nat{}},Nat{}}
+ */
 trait CompoundSort extends Sort {
-  def ctr: String        // sort constructor
-  def params: Seq[Sort]  // sort parameters
+  def ctr: String // sort constructor
+
+  def params: Seq[Sort] // sort parameters
 }
 
 object CompoundSort {
+
   import scala.math.Ordering.Implicits._
+
   def unapply(arg: CompoundSort): Option[(String, Seq[Sort])] = Some(arg.ctr, arg.params)
+
   implicit val ord: Ordering[CompoundSort] = Ordering.by(unapply)
 }
 
 /** A symbol-or-alias is of the form C{s1,...,sn}
-  * where C is called a constructor and s1,...,sn are sort parameters.
-  * In the Semantics of K document, SymbolOrAlias is called the nonterminal <head>
-  */
+ * where C is called a constructor and s1,...,sn are sort parameters.
+ * In the Semantics of K document, SymbolOrAlias is called the nonterminal <head>
+ */
 trait SymbolOrAlias {
   def ctr: String
 
@@ -566,9 +579,12 @@ trait SymbolOrAlias {
 }
 
 object SymbolOrAlias {
+
   import scala.math.Ordering.Implicits._
+
   def unapply(arg: SymbolOrAlias): Option[(String, Seq[Sort])] =
     Some(arg.ctr, arg.params)
+
   implicit val ord: Ordering[SymbolOrAlias] = Ordering.by(unapply)
 }
 
@@ -597,8 +613,8 @@ trait Builders {
                       att: Attributes): Declaration
 
   def HookSortDeclaration(params: Seq[SortVariable],
-                      sort: Sort,
-                      att: Attributes): Declaration
+                          sort: Sort,
+                          att: Attributes): Declaration
 
   def SymbolDeclaration(symbol: Symbol,
                         argSorts: Seq[Sort],
@@ -606,9 +622,9 @@ trait Builders {
                         att: Attributes): Declaration
 
   def HookSymbolDeclaration(symbol: Symbol,
-                        argSorts: Seq[Sort],
-                        returnSort: Sort,
-                        att: Attributes): Declaration
+                            argSorts: Seq[Sort],
+                            returnSort: Sort,
+                            att: Attributes): Declaration
 
   def AliasDeclaration(alias: Alias,
                        argSorts: Seq[Sort],
@@ -651,7 +667,7 @@ trait Builders {
 
   def Iff(s: Sort, _1: Pattern, _2: Pattern): Pattern
 
-  def Exists(s:Sort, v: Variable, p: Pattern): Pattern
+  def Exists(s: Sort, v: Variable, p: Pattern): Pattern
 
   def Forall(s: Sort, v: Variable, p: Pattern): Pattern
 
@@ -663,11 +679,11 @@ trait Builders {
 
   def Rewrites(s: Sort, _1: Pattern, _2: Pattern): Pattern
 
-  def Equals(s: Sort, rs:Sort, _1: Pattern, _2: Pattern): Pattern
+  def Equals(s: Sort, rs: Sort, _1: Pattern, _2: Pattern): Pattern
 
-  def Mem(s: Sort, rs:Sort, p: Pattern, q: Pattern): Pattern
+  def Mem(s: Sort, rs: Sort, p: Pattern, q: Pattern): Pattern
 
-  def DomainValue(s: Sort, str:String): Pattern
+  def DomainValue(s: Sort, str: String): Pattern
 
   // def Subset(s: Sort, rs:Sort, _1: Pattern, _2: Pattern): Pattern