more operations;

--- a/src/Pure/term.scala	Tue Dec 03 15:20:30 2019 +0100
+++ b/src/Pure/term.scala	Tue Dec 03 15:59:01 2019 +0100
@@ -53,6 +53,13 @@
   val dummyT = Type("dummy")
 
   sealed abstract class Term
+  {
+    def head: Term =
+      this match {
+        case App(fun, _) => fun.head
+        case _ => this
+      }
+  }
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
     override def toString: String =