# HG changeset patch
# User wenzelm
# Date 1575385141 -3600
# Node ID 4dfb7c937126254068d0f311d2de4821df80e602
# Parent  35e465677a268a24540359968283a828e4209d8c
more operations;

diff -r 35e465677a26 -r 4dfb7c937126 src/Pure/term.scala
--- 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 =