tuned signature;

--- a/src/Pure/Thy/thy_element.scala	Sun Mar 17 21:26:42 2019 +0100
+++ b/src/Pure/Thy/thy_element.scala	Mon Mar 18 21:05:34 2019 +0100
@@ -30,6 +30,13 @@
         case Some((_, qed)) => Iterator(head, qed)
       }
 
+    def proof_start: Option[A] =
+      proof match {
+        case None => None
+        case Some((Nil, qed)) => Some(qed)
+        case Some((start :: _, _)) => Some(start.head)
+      }
+
     def last: A =
       proof match {
         case None => head