src/Pure/thm_name.scala

 
 
 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
         case ord => ord
       }

       case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
       case _ => Thm_Name(s, 0)
     }
 }
 
-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 + ")"
 
   def flatten: String =