diff --git a/k-distribution/tests/builtins/collections/test-set2list-2.col.out b/k-distribution/tests/builtins/collections/test-set2list-2.col.out
index e698f880343..ff7f12e8d9b 100644
--- a/k-distribution/tests/builtins/collections/test-set2list-2.col.out
+++ b/k-distribution/tests/builtins/collections/test-set2list-2.col.out
@@ -1,6 +1,6 @@
 <k>
-  ListItem ( 4 )
-  ListItem ( 3 )
+  ListItem ( 1 )
   ListItem ( 2 )
-  ListItem ( 1 ) ~> .
+  ListItem ( 3 )
+  ListItem ( 4 ) ~> .
 </k>
diff --git a/k-distribution/tests/builtins/collections/test-set2list-3.col.out b/k-distribution/tests/builtins/collections/test-set2list-3.col.out
index 42af7fc9c87..af1ebe42178 100644
--- a/k-distribution/tests/builtins/collections/test-set2list-3.col.out
+++ b/k-distribution/tests/builtins/collections/test-set2list-3.col.out
@@ -1,5 +1,5 @@
 <k>
-  ListItem ( 4 )
+  ListItem ( 1 )
   ListItem ( 3 )
-  ListItem ( 1 ) ~> .
+  ListItem ( 4 ) ~> .
 </k>
diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala
index f882997bd1e..d3c3685d33f 100644
--- a/kore/src/main/scala/org/kframework/attributes/Att.scala
+++ b/kore/src/main/scala/org/kframework/attributes/Att.scala
@@ -414,6 +414,11 @@ object Att {
     val attMap = union.groupBy({ case ((name, _), _) => name})
     Att(union.filter { key => attMap(key._1._1).size == 1 }.toMap)
   }
+
+  implicit val ord: Ordering[Att] = {
+    import scala.math.Ordering.Implicits._
+    Ordering.by[Att, Seq[(String, String, String)]](att => att.att.iterator.map(k => (k._1._1.key, k._1._2, k._2.toString)).toSeq.sorted)
+  }
 }
 
 trait AttributesToString {
diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala
index 127bb54694c..6931bc8914b 100644
--- a/kore/src/main/scala/org/kframework/definition/outer.scala
+++ b/kore/src/main/scala/org/kframework/definition/outer.scala
@@ -414,18 +414,66 @@ trait Sentence extends HasLocation with HasAtt with AttValue {
   def label: Optional[String] = att.getOptional(Att.LABEL)
 }
 
+object Sentence {
+  implicit val ord = new Ordering[Sentence] {
+    def compare(a: Sentence, b: Sentence): Int = {
+      (a, b) match {
+        case (c:SyntaxSort, d:SyntaxSort) => Ordering[SyntaxSort].compare(c, d)
+        case (c:SortSynonym, d:SortSynonym) => Ordering[SortSynonym].compare(c, d)
+        case (c:SyntaxLexical, d:SyntaxLexical) => Ordering[SyntaxLexical].compare(c, d)
+        case (c:Production, d:Production) => Ordering[Production].compare(c, d)
+        case (c:SyntaxAssociativity, d:SyntaxAssociativity) => Ordering[SyntaxAssociativity].compare(c, d)
+        case (c:SyntaxPriority, d:SyntaxPriority) => Ordering[SyntaxPriority].compare(c, d)
+        case (c:ContextAlias, d:ContextAlias) => Ordering[ContextAlias].compare(c, d)
+        case (c:Context, d:Context) => Ordering[Context].compare(c, d)
+        case (c:Rule, d:Rule) => Ordering[Rule].compare(c, d)
+        case (c:Claim, d:Claim) => Ordering[Claim].compare(c, d)
+        case (_:SyntaxSort, _) => -1
+        case (_, _:SyntaxSort) => 1
+        case (_:SortSynonym, _) => -1
+        case (_, _:SortSynonym) => 1
+        case (_:SyntaxLexical, _) => -1
+        case (_, _:SyntaxLexical) => 1
+        case (_:Production, _) => -1
+        case (_, _:Production) => 1
+        case (_:SyntaxAssociativity, _) => -1
+        case (_, _:SyntaxAssociativity) => 1
+        case (_:SyntaxPriority, _) => -1
+        case (_, _:SyntaxPriority) => 1
+        case (_:ContextAlias, _) => -1
+        case (_, _:ContextAlias) => 1
+        case (_:Context, _) => -1
+        case (_, _:Context) => 1
+        case (_:Rule, _) => -1
+        case (_, _:Rule) => 1
+        case (_:Claim, _) => -1
+        case (_, _:Claim) => 1
+        case (_, _) => throw KEMException.internalError("Cannot order these sentences:\n" + a.toString() + "\n" + b.toString())
+      }
+    }
+  }
+}
+
 // deprecated
 case class Context(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextToString {
   override val isSyntax = false
   override val isNonSyntax = true
   override def withAtt(att: Att) = Context(body, requires, att)
 }
+object Context {
+  implicit val ord: Ordering[Context] = Ordering.by[Context, (K, K, Att)](s => (s.body, s.requires, s.att))
+}
 
 case class ContextAlias(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextAliasToString {
   override val isSyntax = true
   override val isNonSyntax = false
   override def withAtt(att: Att) = ContextAlias(body, requires, att)
 }
+object ContextAlias {
+  implicit val ord: Ordering[ContextAlias] = {
+    Ordering.by[ContextAlias, (K, K, Att)](s => (s.body, s.requires, s.att))
+  }
+}
 
 abstract class RuleOrClaim extends Sentence {
   def body: K
@@ -441,6 +489,11 @@ case class Claim(body: K, requires: K, ensures: K, att: Att = Att.empty) extends
   override def newInstance(body: K, requires: K, ensures: K, att: Att = Att.empty): Claim =
     Claim(body, requires, ensures, att)
 }
+object Claim {
+  implicit val ord: Ordering[Claim] = {
+    Ordering.by[Claim, (K, K, K, Att)](s => (s.body, s.requires, s.ensures, s.att))
+  }
+}
 
 case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends RuleOrClaim with RuleToString with OuterKORE {
   override def withAtt(att: Att): Rule = Rule(body, requires, ensures, att)
@@ -449,18 +502,8 @@ case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends
 }
 
 object Rule {
-  implicit val ord: Ordering[Rule] = new Ordering[Rule] {
-    def compare(a: Rule, b: Rule): Int = {
-      val c1 = Ordering[K].compare(a.body, b.body)
-      if (c1 == 0) {
-        val c2 = Ordering[K].compare(a.requires, b.requires)
-        if (c2 == 0) {
-          Ordering[K].compare(a.ensures, b.ensures)
-        }
-        c2
-      }
-      c1
-    }
+  implicit val ord: Ordering[Rule] = {
+    Ordering.by[Rule, (K, K, K, Att)](r => (r.body, r.requires, r.ensures, r.att))
   }
 }
 
@@ -474,6 +517,12 @@ case class SyntaxPriority(priorities: Seq[Set[Tag]], att: Att = Att.empty)
   override val isNonSyntax = false
   override def withAtt(att: Att) = SyntaxPriority(priorities, att)
 }
+object SyntaxPriority {
+  implicit val ord: Ordering[SyntaxPriority] = {
+    import scala.math.Ordering.Implicits._
+    Ordering.by[SyntaxPriority, (Seq[Seq[Tag]], Att)](s => (s.priorities.map(_.toSeq.sorted), s.att))
+  }
+}
 
 case class SyntaxAssociativity(
                                 assoc: Associativity,
@@ -484,9 +533,19 @@ case class SyntaxAssociativity(
   override val isNonSyntax = false
   override def withAtt(att: Att) = SyntaxAssociativity(assoc, tags, att)
 }
+object SyntaxAssociativity {
+  implicit val ord: Ordering[SyntaxAssociativity] = {
+    import scala.math.Ordering.Implicits._
+    Ordering.by[SyntaxAssociativity, (Associativity, Seq[Tag], Att)](s => (s.assoc, s.tags.toSeq.sorted, s.att))
+  }
+}
 
 case class Tag(name: String) extends TagToString with OuterKORE
 
+object Tag {
+  implicit val ord: Ordering[Tag] = Ordering.by[Tag, String](_.name)
+}
+
 //trait Production {
 //  def sort: Sort
 //  def att: Att
@@ -503,6 +562,13 @@ case class SyntaxSort(params: Seq[Sort], sort: Sort, att: Att = Att.empty) exten
   override val isNonSyntax = false
   override def withAtt(att: Att) = SyntaxSort(params, sort, att)
 }
+object SyntaxSort {
+  implicit val ord: Ordering[SyntaxSort] = {
+    import scala.math.Ordering.Implicits._
+    Ordering.by[SyntaxSort, (Seq[String], String, Att)](s => (s.params.map(_.name), s.sort.name, s.att))
+  }
+}
+
 case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) extends Sentence
   with SortSynonymToString with OuterKORE {
 
@@ -510,6 +576,12 @@ case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) exten
   override val isNonSyntax = false
   override def withAtt(att: Att) = SortSynonym(newSort, oldSort, att)
 }
+object SortSynonym {
+  implicit val ord: Ordering[SortSynonym] = {
+    Ordering.by[SortSynonym, (String, String, Att)](s => (s.newSort.name, s.oldSort.name, s.att))
+  }
+}
+
 case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) extends Sentence
   with SyntaxLexicalToString with OuterKORE {
 
@@ -517,6 +589,11 @@ case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) exte
   override val isNonSyntax = false
   override def withAtt(att: Att) = SyntaxLexical(name, regex, att)
 }
+object SyntaxLexical {
+  implicit val ord: Ordering[SyntaxLexical] = {
+    Ordering.by[SyntaxLexical, (String, String, Att)](s => (s.name, s.regex, s.att))
+  }
+}
 
 case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att)
   extends Sentence with ProductionToString {
@@ -638,10 +715,8 @@ case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, ite
 }
 
 object Production {
-  implicit val ord: Ordering[Production] = new Ordering[Production] {
-    def compare(a: Production, b: Production): Int = {
-      Ordering[Option[String]].compare(a.klabel.map(_.name), b.klabel.map(_.name))
-    }
+  implicit val ord: Ordering[Production] = {
+    Ordering.by[Production, (Option[String], Att)](s => (s.klabel.map(_.name), s.att))
   }
 
   def apply(klabel: KLabel, params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att = Att.empty): Production = {
diff --git a/kore/src/test/scala/org/kframework/definition/OuterTest.scala b/kore/src/test/scala/org/kframework/definition/OuterTest.scala
index c42cb6fa5d8..54e9beb0399 100644
--- a/kore/src/test/scala/org/kframework/definition/OuterTest.scala
+++ b/kore/src/test/scala/org/kframework/definition/OuterTest.scala
@@ -4,6 +4,7 @@ package org.kframework.definition
 
 import org.junit.{Assert, Test}
 import org.kframework.attributes.Att
+import org.kframework.kore.ADT.KToken
 import org.kframework.kore.KORE.Sort
 import org.kframework.kore.KORE.KLabel
 
@@ -90,4 +91,153 @@ class OuterTest {
     val prod2 = Production(Some(KLabel("foo")), Seq(), Sort("Foo"), Seq(), Att.empty.add(Att.KLABEL, "bar"))
     Assert.assertNotEquals(prod1, prod2)
   }
+
+  // Create multiple versions of this sentence with attributes added
+  def toSentenceAttList(sentence: Sentence): List[Sentence] = {
+    val att1 = Att.empty.add(Att.ASSOC).add(Att.BAG)
+    val att2 = Att.empty.add(Att.ASSOC).add(Att.CELL)
+    val att3 = Att.empty.add(Att.BAG).add(Att.CELL)
+    val att4 = Att.empty.add(Att.BAG).add(Att.HOOK, "A")
+    val att5 = Att.empty.add(Att.BAG).add(Att.HOOK, "B")
+    val att6 = Att.empty.add(Att.BAG).add(Att.LABEL, "A")
+    val att7 = Att.empty.add(Att.BAG).add(Att.LABEL, "B")
+    val att8 = Att.empty.add(Att.HOOK, "A").add(Att.LABEL, "B")
+    val att9 = Att.empty.add(Att.HOOK, "B").add(Att.LABEL, "A")
+    val sentenceWithAtt1 = sentence.withAtt(att1)
+    val sentenceWithAtt2 = sentence.withAtt(att2)
+    val sentenceWithAtt3 = sentence.withAtt(att3)
+    val sentenceWithAtt4 = sentence.withAtt(att4)
+    val sentenceWithAtt5 = sentence.withAtt(att5)
+    val sentenceWithAtt6 = sentence.withAtt(att6)
+    val sentenceWithAtt7 = sentence.withAtt(att7)
+    val sentenceWithAtt8 = sentence.withAtt(att8)
+    val sentenceWithAtt9 = sentence.withAtt(att9)
+
+    List(sentenceWithAtt1,
+         sentenceWithAtt2,
+         sentenceWithAtt3,
+         sentenceWithAtt4,
+         sentenceWithAtt5,
+         sentenceWithAtt6,
+         sentenceWithAtt7,
+         sentenceWithAtt8,
+         sentenceWithAtt9)
+  }
+
+  // Asserts that S1 < S2 < ... < Sn
+  // Likewise, Sn > ... > S2 > S1
+  // And Sx = Sx
+  def checkOrdering(sentences: List[Sentence]): Unit = {
+    val ord = Ordering[Sentence]
+    for (remaining <- sentences.tails.filter(_.nonEmpty)) {
+      val head = remaining.head
+      Assert.assertTrue(ord.compare(head, head) == 0)
+      for (sentence <- remaining.tail) {
+        Assert.assertTrue(ord.compare(head, sentence) < 0)
+        Assert.assertTrue(ord.compare(sentence, head) > 0)
+      }
+    }
+  }
+
+  @Test def sentenceOrdering(): Unit = {
+    val sortA = Sort("A")
+    val sortB = Sort("B")
+    val sortC = Sort("C")
+
+    val ktokenA = KToken("A", sortA)
+    val ktokenB = KToken("B", sortA)
+    val ktokenC = KToken("C", sortA)
+
+    val tagA = Tag("A")
+    val tagB = Tag("B")
+    val tagC = Tag("C")
+
+    val syntaxSort1 = SyntaxSort(Seq(sortA, sortC), sortA)
+    val syntaxSort2 = SyntaxSort(Seq(sortA, sortC), sortB)
+    val syntaxSort3 = SyntaxSort(Seq(sortB, sortC), sortA)
+
+    val synonym1 = SortSynonym(sortA, sortA)
+    val synonym2 = SortSynonym(sortA, sortB)
+    val synonym3 = SortSynonym(sortB, sortC)
+
+    val lexical1 = SyntaxLexical("A", "A")
+    val lexical2 = SyntaxLexical("A", "B")
+    val lexical3 = SyntaxLexical("B", "A")
+
+    val production1 = Production(Seq(), sortA, Seq(), Att.empty)
+    val production2 = Production(KLabel("A"), Seq(), sortA, Seq(), Att.empty)
+    val production3 = Production(KLabel("B"), Seq(), sortA, Seq(), Att.empty)
+
+    val syntaxAssoc1 = SyntaxAssociativity(Associativity.Left, Set(tagA))
+    val syntaxAssoc2 = SyntaxAssociativity(Associativity.Left, Set(tagB))
+    val syntaxAssoc3 = SyntaxAssociativity(Associativity.Right, Set(tagA))
+
+    val syntaxPriority1 = SyntaxPriority(Seq(Set(tagB, tagA)))
+    val syntaxPriority2 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagB)))
+    val syntaxPriority3 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagC)))
+    val syntaxPriority4 = SyntaxPriority(Seq(Set(tagA, tagC, tagC), Set(tagB)))
+    val syntaxPriority5 = SyntaxPriority(Seq(Set(tagB)))
+
+    val contextAlias1 = ContextAlias(ktokenA, ktokenA)
+    val contextAlias2 = ContextAlias(ktokenA, ktokenB)
+    val contextAlias3 = ContextAlias(ktokenB, ktokenB)
+
+    val context1 = Context(ktokenA, ktokenA)
+    val context2 = Context(ktokenA, ktokenB)
+    val context3 = Context(ktokenB, ktokenA)
+
+    val rule1 = Rule(ktokenA, ktokenA, ktokenA)
+    val rule2 = Rule(ktokenA, ktokenA, ktokenB)
+    val rule3 = Rule(ktokenA, ktokenA, ktokenC)
+    val rule4 = Rule(ktokenA, ktokenB, ktokenA)
+    val rule5 = Rule(ktokenB, ktokenA, ktokenA)
+
+    val claim1 = Claim(ktokenA, ktokenA, ktokenA)
+    val claim2 = Claim(ktokenA, ktokenA, ktokenB)
+    val claim3 = Claim(ktokenA, ktokenA, ktokenC)
+    val claim4 = Claim(ktokenA, ktokenB, ktokenA)
+    val claim5 = Claim(ktokenB, ktokenA, ktokenA)
+
+    val sentenceList = List(
+      syntaxSort1,
+      syntaxSort2,
+      syntaxSort3,
+      synonym1,
+      synonym2,
+      synonym3,
+      lexical1,
+      lexical2,
+      lexical3,
+      production1,
+      production2,
+      production3,
+      syntaxAssoc1,
+      syntaxAssoc2,
+      syntaxAssoc3,
+      syntaxPriority1,
+      syntaxPriority2,
+      syntaxPriority3,
+      syntaxPriority4,
+      syntaxPriority5,
+      contextAlias1,
+      contextAlias2,
+      contextAlias3,
+      context1,
+      context2,
+      context3,
+      rule1,
+      rule2,
+      rule3,
+      rule4,
+      rule5,
+      claim1,
+      claim2,
+      claim3,
+      claim4,
+      claim5)
+
+    val sentenceListWithAtts = sentenceList.flatMap(toSentenceAttList(_))
+
+    checkOrdering(sentenceListWithAtts)
+  }
 }