diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
index 78c88ebb96b..a3f989da84b 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
@@ -66,11 +66,17 @@ object implementation {
 
     case class StringLiteral(str: String) extends i.StringLiteral
 
-    case class SortVariable(name: String) extends i.SortVariable
+    case class SortVariable(name: String) extends i.SortVariable {
+      override def toString = name
+    }
 
-    case class CompoundSort(ctr: String, params: Seq[i.Sort]) extends i.CompoundSort
+    case class CompoundSort(ctr: String, params: Seq[i.Sort]) extends i.CompoundSort {
+      override def toString = ctr + "{" + params.map(_.toString).mkString(", ") + "}"
+    }
 
-    case class SymbolOrAlias(ctr: String, params: Seq[i.Sort]) extends i.SymbolOrAlias
+    case class SymbolOrAlias(ctr: String, params: Seq[i.Sort]) extends i.SymbolOrAlias {
+      override def toString = ctr + "{" + params.map(_.toString).mkString(", ") + "}"
+    }
 
     case class Symbol(ctr: String, params: Seq[i.Sort]) extends i.Symbol
 
@@ -125,13 +131,13 @@ object implementation {
 
     // def Next(s: i.Sort, _1: i.Pattern): i.Pattern = d.Next(s, _1)
 
-    def Rewrites(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Rewrites(s, _1, _2)
+    def Rewrites(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Rewrites = d.Rewrites(s, _1, _2)
 
     def Ceil(s: i.Sort, rs: i.Sort, p: Pattern): i.Pattern = d.Ceil(s, rs, p)
 
     def Floor(s: i.Sort, rs: i.Sort, p: Pattern): i.Pattern = d.Floor(s, rs, p)
 
-    def Equals(s: i.Sort, rs: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Equals(s, rs, _1, _2)
+    def Equals(s: i.Sort, rs: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Equals = d.Equals(s, rs, _1, _2)
 
     def Mem(s: i.Sort, rs: i.Sort, p: i.Pattern, q: i.Pattern): i.Pattern = d.Mem(s, rs, p, q)
 
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 8a3e10af72f..9737394838a 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
@@ -47,12 +47,7 @@ object SortDeclaration {
   = Some(arg.params, arg.sort, arg.att)
 }
 
-trait HookSortDeclaration extends Declaration {
-  def params: Seq[SortVariable]
-
-  def sort: Sort
-
-  def att: Attributes
+trait HookSortDeclaration extends SortDeclaration {
 }
 
 object HookSortDeclaration {
@@ -75,14 +70,7 @@ object SymbolDeclaration {
   = Some(arg.symbol, arg.argSorts, arg.returnSort, arg.att)
 }
 
-trait HookSymbolDeclaration extends Declaration {
-  def symbol: Symbol
-
-  def argSorts: Seq[Sort]
-
-  def returnSort: Sort
-
-  def att: Attributes
+trait HookSymbolDeclaration extends SymbolDeclaration {
 }
 
 object HookSymbolDeclaration {
@@ -287,18 +275,29 @@ object Floor {
 //   def unapply(arg: Next): Option[(Sort, Pattern)] = Some(arg.s, arg._1)
 // }
 
+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.
   */
-trait Rewrites extends Pattern {
+trait Rewrites extends Pattern with GeneralizedRewrite {
   def s: Sort // the sort of the two patterns P and Q
 
+  def sort = s
+
   def _1: Pattern
 
   def _2: Pattern
+
+  def getLeftHandSide = Seq(_1)
+  def getRightHandSide = _2
 }
 
 object Rewrites {
@@ -306,14 +305,22 @@ object Rewrites {
     Some(arg.s, arg._1, arg._2)
 }
 
-trait Equals extends Pattern {
+trait Equals extends Pattern with GeneralizedRewrite {
   def s: Sort // the sort of the two patterns that are being compared
 
   def rs: Sort // the sort of the context where the equality pattern is being placed
 
+  def sort = rs
+
   def _1: Pattern
 
   def _2: Pattern
+
+  def getLeftHandSide = _1 match {
+    case Application(_, ps) => ps
+  }
+
+  def getRightHandSide = _2
 }
 
 object Equals {