# HG changeset patch
# User wenzelm
# Date 1136332362 -3600
# Node ID 6b4570eb22d222903ace312d1cdfcc375263999e
# Parent  05b3f033c72db7ee7121ac84915199095ab4b703
adapted Toplevel.Proof;

diff -r 05b3f033c72d -r 6b4570eb22d2 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Jan 04 00:52:40 2006 +0100
+++ b/src/Pure/proof_general.ML	Wed Jan 04 00:52:42 2006 +0100
@@ -1197,7 +1197,7 @@
   end
 
   val topnode = Toplevel.node_of o Toplevel.get_state
-  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
+  fun topproofpos () = (case topnode() of Toplevel.Proof (h, _) => SOME(ProofHistory.position h)
                                         | _ => NONE) handle Toplevel.UNDEF => NONE
 in