src/Pure/term.scala
changeset 71221 4dfb7c937126
parent 70916 4c15217d6266
child 71601 97ccf48c2f0c
equal deleted inserted replaced
71219:35e465677a26 71221:4dfb7c937126
    51       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
    51       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
    52   }
    52   }
    53   val dummyT = Type("dummy")
    53   val dummyT = Type("dummy")
    54 
    54 
    55   sealed abstract class Term
    55   sealed abstract class Term
       
    56   {
       
    57     def head: Term =
       
    58       this match {
       
    59         case App(fun, _) => fun.head
       
    60         case _ => this
       
    61       }
       
    62   }
    56   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
    63   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
    57   {
    64   {
    58     override def toString: String =
    65     override def toString: String =
    59       if (this == dummy) "_"
    66       if (this == dummy) "_"
    60       else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
    67       else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"