src/Pure/thm_name.scala
changeset 75393 87ebf5a50283
parent 70580 e6101f131d0d
child 79376 b275e3379024
--- a/src/Pure/thm_name.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/thm_name.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -10,10 +10,8 @@
 import scala.math.Ordering
 
 
-object Thm_Name
-{
-  object Ordering extends scala.math.Ordering[Thm_Name]
-  {
+object Thm_Name {
+  object Ordering extends scala.math.Ordering[Thm_Name] {
     def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int =
       thm_name1.name compare thm_name2.name match {
         case 0 => thm_name1.index compare thm_name2.index
@@ -32,8 +30,7 @@
     }
 }
 
-sealed case class Thm_Name(name: String, index: Int)
-{
+sealed case class Thm_Name(name: String, index: Int) {
   def print: String =
     if (name == "" || index == 0) name
     else name + "(" + index + ")"