# HG changeset patch
# User wenzelm
# Date 1552939534 -3600
# Node ID 7837309d633a6e5f19d1a39b02c0b8ec811ceea6
# Parent  66c4567664b5538402366b1ddb7538249c64804b
tuned signature;

diff -r 66c4567664b5 -r 7837309d633a src/Pure/Thy/thy_element.scala
--- 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